Bug #545: CVC3 wastes some time after it has already given an answer - BLAST - Open-Source Projects

Actions

Copy link

Bug #545

closed

CVC3 wastes some time after it has already given an answer

Added by Pavel Shved over 13 years ago. Updated over 12 years ago.

Status:

Rejected

Priority:

Low

Assignee:

Pavel Shved

Category:

Target version:

2.6

Start date:

11/14/2010

Due date:

% Done:

Estimated time:

Detected in build:

cvc3: 0e2a0c93

Platform:

Published in build:

Description

I noticed that after CVC3 already printed its answer (whether the input formula is SAT), it spends some time doing something.

For example, I run the file attached (smt_query_long) with the following command:

cvc3 -lang smtlib  < smt_query_long

The program runs for 18 seconds (and takes 2 Gb of memory on my 64-bit machine). However, it prints its answer on 12th second, wasting 30% of its time for doing...nothing. For all this period, the two-gigabyte memory blob hangs in RAM, shrinking only for a tiny bit.

I bet the issues is how CVC3's memory allocator works. Could this be optimized somehow?

I use CVC3 revision 0e2a0c93 (for-blast branch).

Files

smt_query_long (89.5 KB) smt_query_long

SMTlib query that runs for a long time

Pavel Shved, 11/14/2010 01:49 PM

Related issues 1 (0 open — 1 closed)

Actions

Copy link

Updated by Evgeny Novikov over 13 years ago

Can we speed up CVC3 again or we can't after #546 resolution?

Actions

Copy link

Updated by Pavel Shved over 13 years ago

I'll run a couple of experiments by tomorrow.

Actions

Copy link

Updated by Pavel Shved over 13 years ago

Category set to BLAST
Status changed from New to Rejected
Assignee set to Pavel Shved
Priority changed from Normal to Low

I ran a couple of experiments, and here are my conclusions.

First, solvers are called from BLAST via a special layer. This layer invokes solver concurrently, and BLAST doesn't have to wait until the solver finishes its work, it can proceed as soon as it got a result from it. So, unless we have a congestion of solver requests (which is the case when we collect useful blocks, but is not one if we iterate and refine abstraction) at this layer, this bug doesn't make it slower.

Second, I tried to run this query with the options from bug #546 (-lang smtlib -quant-complete-inst -quant-new -quant-max-IL 1). The program runs in less than a half of a second, which makes it uneasy to measure. I could have written a program to do the measurement, but it's not necessary: taking the thoughts in the previous paragraph into account, if solver works for such a short time, it's not an issue at all.

Well, at least it's not the best opportunity to optimize.

Actions

Copy link