Project

General

Profile

Actions

Bug #545

closed

CVC3 wastes some time after it has already given an answer

Added by Pavel Shved almost 14 years ago. Updated about 13 years ago.

Status:
Rejected
Priority:
Low
Assignee:
Category:
-
Target version:
Start date:
11/14/2010
Due date:
% Done:

0%

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 open1 closed)

Blocks BLAST - Bug #544: CVC3 is too slow and greedy in memory consumptionClosedPavel Shved11/14/2010

Actions
Actions #1

Updated by Evgeny Novikov almost 14 years ago

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

Actions #2

Updated by Pavel Shved almost 14 years ago

I'll run a couple of experiments by tomorrow.

Actions #3

Updated by Pavel Shved almost 14 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 #4

Updated by Pavel Shved about 13 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)
Actions #5

Updated by Pavel Shved about 13 years ago

  • Target version set to 2.6
Actions

Also available in: Atom PDF