cvc5.git
12 years agobetter documentation, allow examples to be installed, etc
Morgan Deters [Wed, 3 Oct 2012 21:41:15 +0000 (21:41 +0000)]
better documentation, allow examples to be installed, etc

12 years agoNew model code, mostly workin
Clark Barrett [Wed, 3 Oct 2012 21:28:11 +0000 (21:28 +0000)]
New model code, mostly workin

12 years agonew README and INSTALL files
Morgan Deters [Wed, 3 Oct 2012 21:27:11 +0000 (21:27 +0000)]
new README and INSTALL files

12 years agoadded support for interrupting TheoryBV
Liana Hadarean [Wed, 3 Oct 2012 19:41:45 +0000 (19:41 +0000)]
added support for interrupting TheoryBV

12 years ago--wait-to-join / --no-wait-to-join option
Kshitij Bansal [Wed, 3 Oct 2012 19:05:32 +0000 (19:05 +0000)]
--wait-to-join / --no-wait-to-join option

workaround option till we fix bug 409. for now, I have kept --wait-to-join to
be default (old behavior). We could technically make --no-wait-to-join the
default when using non-incremental mode, but still possible for problems at
exit I think

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoadding ::getBooleanVariables to the PropEngine
Dejan Jovanović [Wed, 3 Oct 2012 17:59:33 +0000 (17:59 +0000)]
adding ::getBooleanVariables to the PropEngine
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables

12 years ago* re-enable some Z3 extended commands:
Morgan Deters [Tue, 2 Oct 2012 22:13:12 +0000 (22:13 +0000)]
* re-enable some Z3 extended commands:
  declare-const
  declare-funs
  declare-preds
  define
  simplify

* don't output --help on bad options, just invite user to try --help

* Datatypes from SMT2 parser now name the tester is-cons (e.g.)

* unknown results produce models, --check-model doesn't fail hard for
  incorrect unknown models.  removed the assert that kept arithmetic
  from producing models if it saw nonlinear

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoworkaround for a nasty CLN bug
Morgan Deters [Tue, 2 Oct 2012 02:57:59 +0000 (02:57 +0000)]
workaround for a nasty CLN bug

12 years ago"Fix" (disable) portfolio when using quantifiers
Kshitij Bansal [Mon, 1 Oct 2012 22:11:26 +0000 (22:11 +0000)]
"Fix" (disable) portfolio when using quantifiers

Other changes:
* fix compile error in smt_engine in debug builds
* add getLogicInfo in smt_engine
* remove "empty-channel" and "disable-lemma-sharing" debug tags

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agomake sure to mark LogicInfo as CVC4_PUBLIC
Morgan Deters [Mon, 1 Oct 2012 21:10:26 +0000 (21:10 +0000)]
make sure to mark LogicInfo as CVC4_PUBLIC

12 years agofix for dejan: term ITEs now dumped correctly
Morgan Deters [Mon, 1 Oct 2012 21:10:04 +0000 (21:10 +0000)]
fix for dejan: term ITEs now dumped correctly

12 years agoinitial draft of skolemization during pre-processing, made simple cliques the default...
Andrew Reynolds [Mon, 1 Oct 2012 19:55:15 +0000 (19:55 +0000)]
initial draft of skolemization during pre-processing, made simple cliques the default option for uf strong solver

12 years agominor changes to arithmetic assertions involving nonlinearity and models (related...
Morgan Deters [Sun, 30 Sep 2012 23:20:49 +0000 (23:20 +0000)]
minor changes to arithmetic assertions involving nonlinearity and models (related to bug 405)

12 years agominor fixes to pickler (hopefully fixes Debian build from last night)
Morgan Deters [Sun, 30 Sep 2012 23:16:49 +0000 (23:16 +0000)]
minor fixes to pickler (hopefully fixes Debian build from last night)

12 years agorelease notes
Morgan Deters [Sun, 30 Sep 2012 22:29:57 +0000 (22:29 +0000)]
release notes

12 years agoCalling the setIncompleteness() flag on all full checks once a non-linear term has...
Tim King [Sat, 29 Sep 2012 20:42:16 +0000 (20:42 +0000)]
Calling the setIncompleteness() flag on all full checks once a non-linear term has been seen.

12 years agoFix a few segfaults in driver.
Morgan Deters [Sat, 29 Sep 2012 17:48:46 +0000 (17:48 +0000)]
Fix a few segfaults in driver.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agodraft RELEASE-NOTES file, and minor release stuff
Morgan Deters [Sat, 29 Sep 2012 16:19:01 +0000 (16:19 +0000)]
draft RELEASE-NOTES file, and minor release stuff

12 years agofixes to "make distclean" and C compatibility bindings; should fix the broken builds...
Morgan Deters [Sat, 29 Sep 2012 13:53:01 +0000 (13:53 +0000)]
fixes to "make distclean" and C compatibility bindings; should fix the broken builds last night

12 years agofixes to "make distclean" and C compatibility bindings; should fix the broken builds...
Morgan Deters [Sat, 29 Sep 2012 13:52:53 +0000 (13:52 +0000)]
fixes to "make distclean" and C compatibility bindings; should fix the broken builds last night

12 years agoThis commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and DIVISION...
Tim King [Sat, 29 Sep 2012 07:19:28 +0000 (07:19 +0000)]
This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and DIVISION. Improves support for non-linear monomials in getEqualityStatus(). Fixes bug 405.

12 years agoSome fixes to portfolio
Kshitij Bansal [Fri, 28 Sep 2012 22:46:09 +0000 (22:46 +0000)]
Some fixes to portfolio

* respect output lang
* fix export variable for BOUND_VARIABLE
* support export of SUBRANGE_TYPE
* statistic for lastWinner, other minor stat changes
* fix running of multiple threads on checsat/query
* changes of Assert -> assert which became private
* fix some destruction time order issues
* fix Pickler with AssertionException going private

Fixed by not fixing:
* portfolio+datatypes does not work
  - added ExportUnsupportedException to more places, switches
    to sequential
   (still TODO / decide : not switch silently, but print error)
   > note: this exception now needs to be (and is) defined in expr.h

Known issues:
* problems in portfolio+quantifiers
   - at least some problems appear to be because of static variables
   (will be later "fixed" like the datatypes)

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agofix distribution of cvc4_assert.i
Morgan Deters [Fri, 28 Sep 2012 22:31:12 +0000 (22:31 +0000)]
fix distribution of cvc4_assert.i

12 years agofixes for compatibility (i.e., CVC3) Java bindings
Morgan Deters [Fri, 28 Sep 2012 20:34:00 +0000 (20:34 +0000)]
fixes for compatibility (i.e., CVC3) Java bindings

12 years agorename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to make it...
Morgan Deters [Fri, 28 Sep 2012 20:14:40 +0000 (20:14 +0000)]
rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to make it unambiguous for case-insensitive filesystems like on Mac.  Fixes Mac builds

12 years agosome fixes to build system
Morgan Deters [Fri, 28 Sep 2012 19:20:02 +0000 (19:20 +0000)]
some fixes to build system

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agofix production-build linking error
Morgan Deters [Fri, 28 Sep 2012 18:22:29 +0000 (18:22 +0000)]
fix production-build linking error

12 years agoPublic interface review items:
Morgan Deters [Fri, 28 Sep 2012 17:29:01 +0000 (17:29 +0000)]
Public interface review items:

* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
  or a public exception type.
* auto-generated documentation for Smt options and internal options

Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.

12 years ago* fix compatibility library naming for SMT-LIBv1
Morgan Deters [Fri, 28 Sep 2012 16:46:13 +0000 (16:46 +0000)]
* fix compatibility library naming for SMT-LIBv1
* change name of JNI library to "libcvc4jni", which works better with Java's
  System.loadLibrary().

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years ago* Rename SMT parts (printer, parser) to SMT1
Morgan Deters [Thu, 27 Sep 2012 22:04:38 +0000 (22:04 +0000)]
* Rename SMT parts (printer, parser) to SMT1
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1

* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
  looks like either SMT-LIB v1 or v2

* Other associated changes

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agofinally, a portable solution
Morgan Deters [Thu, 27 Sep 2012 20:11:59 +0000 (20:11 +0000)]
finally, a portable solution

12 years agofix for non-Mac
Morgan Deters [Thu, 27 Sep 2012 20:10:00 +0000 (20:10 +0000)]
fix for non-Mac

12 years agospeed up mkoptions script (esp. on Macs)
Morgan Deters [Thu, 27 Sep 2012 20:07:21 +0000 (20:07 +0000)]
speed up mkoptions script (esp. on Macs)

12 years agobetter progress indicator for mkoptions
Morgan Deters [Thu, 27 Sep 2012 18:41:20 +0000 (18:41 +0000)]
better progress indicator for mkoptions

12 years agodisable building of cvc3_george system-test object (which isn't used yet anyway,...
Morgan Deters [Wed, 26 Sep 2012 22:22:09 +0000 (22:22 +0000)]
disable building of cvc3_george system-test object (which isn't used yet anyway, and required ~10 minutes to build with -O3).

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoFinish off SEXPR kind work.
Morgan Deters [Wed, 26 Sep 2012 22:00:19 +0000 (22:00 +0000)]
Finish off SEXPR kind work.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoupdates to model generation : do not modify equality engine during getValue, other...
Andrew Reynolds [Wed, 26 Sep 2012 21:44:22 +0000 (21:44 +0000)]
updates to model generation : do not modify equality engine during getValue, other minor changes, still problems with constants not being specified for some eq classes

12 years agoFix a handful of things for Mac, and Java bindings.
Morgan Deters [Wed, 26 Sep 2012 18:51:48 +0000 (18:51 +0000)]
Fix a handful of things for Mac, and Java bindings.

Also add a "mac-build" script that sets up prerequisites for Mac.

12 years agobug #398 test (bug was resolved last night), and a script to download all bug attachm...
Morgan Deters [Wed, 26 Sep 2012 16:42:40 +0000 (16:42 +0000)]
bug #398 test (bug was resolved last night), and a script to download all bug attachments from bugzilla and put them in the tree

12 years agoFix type checking for define-funs (resolves bug 398).
Morgan Deters [Wed, 26 Sep 2012 03:50:57 +0000 (03:50 +0000)]
Fix type checking for define-funs (resolves bug 398).

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoThe Tuesday Afternoon Catch-All Commit (TACAC):
Morgan Deters [Wed, 26 Sep 2012 03:07:01 +0000 (03:07 +0000)]
The Tuesday Afternoon Catch-All Commit (TACAC):

* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)

* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).

* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agofix
Morgan Deters [Tue, 25 Sep 2012 20:32:18 +0000 (20:32 +0000)]
fix

12 years agofix some Mac issues
Morgan Deters [Tue, 25 Sep 2012 18:57:48 +0000 (18:57 +0000)]
fix some Mac issues

12 years agosome buggy examples for incrementality, and make bug326 run as part of make regress...
Morgan Deters [Tue, 25 Sep 2012 15:16:41 +0000 (15:16 +0000)]
some buggy examples for incrementality, and make bug326 run as part of make regress, because the bug was fixed.

Also make QuantifiersModule's destructor virtual (it has virtual members).

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agosome api changes
Dejan Jovanović [Mon, 24 Sep 2012 20:55:58 +0000 (20:55 +0000)]
some api changes

12 years agoFix the memout issue seen in recent nightly regressions (was due to a
Morgan Deters [Mon, 24 Sep 2012 18:37:22 +0000 (18:37 +0000)]
Fix the memout issue seen in recent nightly regressions (was due to a
Statistics-printing problem, limited to certain benchmarks).

Mark some unlabeled header files "cvc4_private.h".

Other minor cleanup.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoSeparate public-facing and internal-facing interfaces to Statistics.
Morgan Deters [Sat, 22 Sep 2012 21:10:51 +0000 (21:10 +0000)]
Separate public-facing and internal-facing interfaces to Statistics.

The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).

The StatisticsRegistry is now internal-only.  However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).

This is part of the ongoing effort to clean up the public interface.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoanother fix for the equality class iterator
Dejan Jovanović [Sat, 22 Sep 2012 14:34:52 +0000 (14:34 +0000)]
another fix for the equality class iterator

12 years agoFixes for datatype dumping and printing. Add a new test case for dumping.
Morgan Deters [Fri, 21 Sep 2012 21:09:18 +0000 (21:09 +0000)]
Fixes for datatype dumping and printing.  Add a new test case for dumping.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoSMT-LIBv2 compliance updates:
Morgan Deters [Fri, 21 Sep 2012 20:34:19 +0000 (20:34 +0000)]
SMT-LIBv2 compliance updates:

* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
  TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default

Also:

* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agobetter verbosity support (so it's sensible when the library is used via the API)
Morgan Deters [Fri, 21 Sep 2012 10:24:08 +0000 (10:24 +0000)]
better verbosity support (so it's sensible when the library is used via the API)

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agomap C++ exceptions to Java exceptions correctly when they are thrown, and give a...
Morgan Deters [Thu, 20 Sep 2012 18:59:26 +0000 (18:59 +0000)]
map C++ exceptions to Java exceptions correctly when they are thrown, and give a build error for Java component if it is misconfigured

12 years agosome bugfixes that come as a result of debugging some CASCADE/C stuff..
Morgan Deters [Thu, 20 Sep 2012 13:36:12 +0000 (13:36 +0000)]
some bugfixes that come as a result of debugging some CASCADE/C stuff..

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoGeneral subscriber infrastructure for NodeManager, as discussed in the
Morgan Deters [Wed, 19 Sep 2012 21:21:00 +0000 (21:21 +0000)]
General subscriber infrastructure for NodeManager, as discussed in the
meeting last week.  The SmtEngine now subscribes to NodeManager events,
does appropriate dumping of variable declarations, and notifies the Model
class.

The way to create a skolem is now:

  nodeManager->mkSkolem("myvar_$$", TypeNode, "is a variable created by the theory of Foo")

The first argument is the name of the skolem, and the (optional) "$$" is a
placeholder for the node id (to get a unique name).  Without a "$$", a "_$$"
is automatically appended to the given name.

The second argument is the type.

The (optional, but recommended) third argument is a comment, used by the
dump infrastructure to indicate what the variable is for / who owns it.

An optional fourth argument (not shown) allows you to specify flags that
control the behavior (e.g., don't do notification, and/or don't make a
unique name).  Look at the documentation for details on these.

In particular, the above means you can't just do a mkSkolem(boolType) for
example---you have to specify a name and (hopefully also,
but it's optional) a comment.  This leads to easier debugging than the
anonymous skolems before, since we'll be able to track where the skolems
came from.

Much of the Model and Dump stuff, as well as some Command stuff, is cleaned up
by this commit.  Some remains to be cleaned up.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agofix subtle bug in NodeValue::toStream()
Morgan Deters [Wed, 19 Sep 2012 21:11:41 +0000 (21:11 +0000)]
fix subtle bug in NodeValue::toStream()

12 years agofix for bug 370.
Dejan Jovanović [Wed, 19 Sep 2012 20:06:27 +0000 (20:06 +0000)]
fix for bug 370.
some internal nodes in eq engine were treated as constants incorrectly

12 years agoChanging the equality engines's euivalence class iterator. Andy please check if this...
Dejan Jovanović [Wed, 19 Sep 2012 18:56:41 +0000 (18:56 +0000)]
Changing the equality engines's euivalence class iterator. Andy please check if this does what you want it to do.

12 years agoSMT-LIBv2 compliance regarding outputting "unknown".
Morgan Deters [Tue, 18 Sep 2012 14:50:45 +0000 (14:50 +0000)]
SMT-LIBv2 compliance regarding outputting "unknown".

Thanks to Peter Collingbourne for the report, and the patch!

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agospeed up option-file generation on Mac OS by an order of magnitude
Morgan Deters [Mon, 17 Sep 2012 22:38:32 +0000 (22:38 +0000)]
speed up option-file generation on Mac OS by an order of magnitude

12 years agomore bindings fixes
Morgan Deters [Mon, 17 Sep 2012 21:14:37 +0000 (21:14 +0000)]
more bindings fixes

12 years agominor fix for models, added simple cliques option for uf strong solver
Andrew Reynolds [Mon, 17 Sep 2012 16:39:48 +0000 (16:39 +0000)]
minor fix for models, added simple cliques option for uf strong solver

12 years agoenable bug regression for bug 382
Morgan Deters [Sun, 16 Sep 2012 01:24:24 +0000 (01:24 +0000)]
enable bug regression for bug 382

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agostore values returned by get-value in TheoryModel::d_reps if necessary, fixes bug...
Andrew Reynolds [Sun, 16 Sep 2012 00:49:04 +0000 (00:49 +0000)]
store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382.

12 years agominor interface improvements, compliance fixes
Morgan Deters [Sat, 15 Sep 2012 22:41:03 +0000 (22:41 +0000)]
minor interface improvements, compliance fixes

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoanother bindings fix (should fix debian build)
Morgan Deters [Sat, 15 Sep 2012 22:32:34 +0000 (22:32 +0000)]
another bindings fix (should fix debian build)

12 years agobug testcase for model generation
Morgan Deters [Sat, 15 Sep 2012 22:27:23 +0000 (22:27 +0000)]
bug testcase for model generation

12 years agoa fix for the java bindings for wei
Morgan Deters [Fri, 14 Sep 2012 19:25:58 +0000 (19:25 +0000)]
a fix for the java bindings for wei

12 years agoFix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).
Morgan Deters [Fri, 14 Sep 2012 17:16:26 +0000 (17:16 +0000)]
Fix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).

Also fix an issue where --check-model didn't take user define-funs into account.

Also make preprocessing a bit more chatty (with -v -v).

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoFix a few minor issues in options processing, improving usability, consistency, error...
Morgan Deters [Fri, 14 Sep 2012 15:13:37 +0000 (15:13 +0000)]
Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation.

12 years agoensure that get-value and get-model are consistent, rewrite function value bodies...
Andrew Reynolds [Thu, 13 Sep 2012 20:39:13 +0000 (20:39 +0000)]
ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output

12 years agoAdding model assertions after SAT responses.
Morgan Deters [Wed, 12 Sep 2012 20:31:59 +0000 (20:31 +0000)]
Adding model assertions after SAT responses.

To enable, use --check-models.  Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not.  This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.

By default, --check-models is quiet (no output unless it detects a problem).  That allows regression runs to pass unless there are problems:

  make regress CVC4_REGRESSION_ARGS=--check-models

To see it work, use -v in addition to --check-models.

There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.

--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models.  This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).

Also:

* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)

12 years agoadded getCardinality to model
Andrew Reynolds [Tue, 11 Sep 2012 23:44:49 +0000 (23:44 +0000)]
added getCardinality to model

12 years agoPartially reverting the changes made in 4308. There is now both an Expr and Node...
Tim King [Tue, 11 Sep 2012 00:20:51 +0000 (00:20 +0000)]
Partially reverting the changes made in 4308. There is now both an Expr and Node version of getValue() in TheoryModel.

12 years agomodified getValue to return Expr instead of Node
Andrew Reynolds [Mon, 10 Sep 2012 22:29:17 +0000 (22:29 +0000)]
modified getValue to return Expr instead of Node

12 years agoFixed an error in the rewriter Pascal pointed out. This was in effectively dead code...
Tim King [Mon, 10 Sep 2012 20:38:35 +0000 (20:38 +0000)]
Fixed an error in the rewriter Pascal pointed out. This was in effectively dead code. (Nobody internally made minus nodes.)

12 years agolist portfolio_util.h in Makefile, so it gets distributed (fixes debian build)
Morgan Deters [Mon, 10 Sep 2012 14:26:48 +0000 (14:26 +0000)]
list portfolio_util.h in Makefile, so it gets distributed (fixes debian build)

12 years agoAdd [*] footnotes to --help output indicating for many options --FOO that there are...
Morgan Deters [Sat, 8 Sep 2012 23:00:23 +0000 (23:00 +0000)]
Add [*] footnotes to --help output indicating for many options --FOO that there are --no-FOO variants.

12 years agoSome minor changes after reviewing the portfolio "unified driver" commit.
Morgan Deters [Sat, 8 Sep 2012 22:31:44 +0000 (22:31 +0000)]
Some minor changes after reviewing the portfolio "unified driver" commit.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoSingle driver for both sequential and portfolio
Kshitij Bansal [Sat, 8 Sep 2012 14:25:25 +0000 (14:25 +0000)]
Single driver for both sequential and portfolio

A "command executer" layer between parsing commands and invoking them.

New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.

12 years agoallow SmtEngine::setOption() for trace and debug tags
Morgan Deters [Thu, 6 Sep 2012 22:15:56 +0000 (22:15 +0000)]
allow SmtEngine::setOption() for trace and debug tags

12 years agofixes to the compatibility layer; this fixes the broken system test
Morgan Deters [Thu, 6 Sep 2012 20:05:20 +0000 (20:05 +0000)]
fixes to the compatibility layer; this fixes the broken system test

12 years agoRemove SmtEngine::getStackLevel(), which exposed implementation details and was only...
Morgan Deters [Thu, 6 Sep 2012 02:38:39 +0000 (02:38 +0000)]
Remove SmtEngine::getStackLevel(), which exposed implementation details and was only used by the compatibility layer.

Make SmtEngine::internalPop() delay popping.  This fixes a bug in model generation.

12 years agoadd --incremental to --smtlib2 compliance mode (thanks Peter Collingbourne)
Morgan Deters [Thu, 6 Sep 2012 00:53:18 +0000 (00:53 +0000)]
add --incremental to --smtlib2 compliance mode (thanks Peter Collingbourne)

12 years agoadd a THANKS file for listing external source code contributors
Morgan Deters [Wed, 5 Sep 2012 20:51:34 +0000 (20:51 +0000)]
add a THANKS file for listing external source code contributors

12 years agoAccepted some patches from the Multicore Programming Group at Imperial College London...
Morgan Deters [Tue, 4 Sep 2012 22:22:41 +0000 (22:22 +0000)]
Accepted some patches from the Multicore Programming Group at Imperial College London (via Peter Collingbourne):

cvc4-0001-Look-for-cxxtestgen-as-well-as-cxxtestgen.pl-and-cxx.patch
* better checking for cxxtest
cvc4-0002-Do-not-read-an-additional-command-after-failure.patch
* more correct failure behavior for interactive tools
cvc4-0003-Only-exit-when-encountering-a-CommandFailure.patch
* don't consider "unsupported" as a failure (accepted with modifications)
cvc4-0004-Produce-SMT-LIB-v2-conformant-output-for-get-info.patch
* better get-info responses (accepted with modifications)

These patches will help the group build Boogie support for CVC4.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agominor cleanup leftover from fmf-devel
Andrew Reynolds [Mon, 3 Sep 2012 17:52:07 +0000 (17:52 +0000)]
minor cleanup leftover from fmf-devel

12 years agomerge from fmf-devel branch. more updates to models: now with collectModelInfo with...
Andrew Reynolds [Fri, 31 Aug 2012 16:48:20 +0000 (16:48 +0000)]
merge from fmf-devel branch.  more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes.  Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

12 years agoset the default expression-printing depth to "unlimited"
Morgan Deters [Thu, 30 Aug 2012 21:13:44 +0000 (21:13 +0000)]
set the default expression-printing depth to "unlimited"

12 years ago* Numerous documentation fixes (fix doxygen warnings, add missing documentation,...
Morgan Deters [Wed, 29 Aug 2012 20:36:35 +0000 (20:36 +0000)]
* Numerous documentation fixes (fix doxygen warnings, add missing documentation, etc.).

* Remove sat_module.cpp, which was no longer used (was previously refactored?)

12 years agoTo the build system:
Morgan Deters [Wed, 29 Aug 2012 11:50:15 +0000 (11:50 +0000)]
To the build system:

* Fix "make distclean."  This should fix the "local regressions fail"
  that caused documentation, debian, and "distcheck" nightly build targets
  to fail.

* "make clean" now removes some options stuff that previously required a
  "make distclean."

* Cosmetic and portability adjustments.

12 years agotest summaries for automake 1.12 test harness
Morgan Deters [Tue, 28 Aug 2012 18:38:19 +0000 (18:38 +0000)]
test summaries for automake 1.12 test harness

12 years agofix a bug in CLN rational printing where the base was ignored (was causing the new...
Morgan Deters [Tue, 28 Aug 2012 17:14:59 +0000 (17:14 +0000)]
fix a bug in CLN rational printing where the base was ignored (was causing the new CVC3-compatibility-API system test to fail)

12 years agofix regression tests for automake 1.11 and automake 1.12---both versions should work now
Morgan Deters [Tue, 28 Aug 2012 15:26:46 +0000 (15:26 +0000)]
fix regression tests for automake 1.11 and automake 1.12---both versions should work now

12 years agoImproved compatibility layer, now supports quantifiers. Also incorporates
Morgan Deters [Tue, 28 Aug 2012 01:10:16 +0000 (01:10 +0000)]
Improved compatibility layer, now supports quantifiers.  Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.

12 years agofixes for Mac and automake 1.12 detection
Morgan Deters [Tue, 28 Aug 2012 00:44:55 +0000 (00:44 +0000)]
fixes for Mac and automake 1.12 detection

12 years agofix a destruction-order issue that was (1) causing valgrind to complain loudly about...
Morgan Deters [Mon, 27 Aug 2012 20:37:17 +0000 (20:37 +0000)]
fix a destruction-order issue that was (1) causing valgrind to complain loudly about invalid reads and writes, and (2) apparently causing problems deleting the decision engine (which is now being properly deleted)

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years ago* Reversing commit r4258 (which disabled failing regressions). Fixed the problem...
Morgan Deters [Mon, 27 Aug 2012 19:27:28 +0000 (19:27 +0000)]
* Reversing commit r4258 (which disabled failing regressions).  Fixed the problem so they're no longer failing (in the quantifiers rewriter).  Resolves bug #381.

* Added LAMBDA kind and type rule, and Node::isClosure().

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agominor, lying around in a wd (related to investigating bug 374)
Kshitij Bansal [Sun, 26 Aug 2012 19:53:14 +0000 (19:53 +0000)]
minor, lying around in a wd (related to investigating bug 374)

12 years agodisabling failing regressions
Kshitij Bansal [Sun, 26 Aug 2012 19:39:03 +0000 (19:39 +0000)]
disabling failing regressions

12 years agoArray constants finished and working. Unit tests for array constants.
Clark Barrett [Sun, 26 Aug 2012 17:56:55 +0000 (17:56 +0000)]
Array constants finished and working.  Unit tests for array constants.