summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-10-06* Include a few bug testcases for resolved bugs.Morgan Deters
* Fix error message if you POP beyond the bottom user stack frame. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
* Ensure Rewriter::init() is called before ::rewrite(). The array type enumerator recently gave us an end-run around ::init(). TheoryEngine no longer calls these, they're done via static initialization. * Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-05fix \fileMorgan Deters
2012-10-05Bug-related:Morgan Deters
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-04disable model-generation by default in cvc3 compatibility layer. should fix ↵Morgan Deters
system test failure (bug 414).
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-10-04IllegalArgumentException in java needs to be named ↵Morgan Deters
"CVC4IllegalArgumentException" to avoid a name clash with java.lang.IllegalArgumentException, which isn't easily avoided, due to swig-autogenerated code that uses it unqualified. X-(
2012-10-03minor fix for mbqi in finite model findingAndrew Reynolds
2012-10-03implemented collectModelInfo for TheoryBVLiana Hadarean
2012-10-03updates to contrib scripts to match docsMorgan Deters
2012-10-03better documentation, allow examples to be installed, etcMorgan Deters
2012-10-03New model code, mostly workinClark Barrett
2012-10-03new README and INSTALL filesMorgan Deters
2012-10-03added support for interrupting TheoryBVLiana Hadarean
2012-10-03--wait-to-join / --no-wait-to-join optionKshitij Bansal
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.)
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables
2012-10-02* re-enable some Z3 extended commands:Morgan Deters
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.)
2012-10-02workaround for a nasty CLN bugMorgan Deters
2012-10-01"Fix" (disable) portfolio when using quantifiersKshitij Bansal
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.)
2012-10-01make sure to mark LogicInfo as CVC4_PUBLICMorgan Deters
2012-10-01fix for dejan: term ITEs now dumped correctlyMorgan Deters
2012-10-01initial draft of skolemization during pre-processing, made simple cliques ↵Andrew Reynolds
the default option for uf strong solver
2012-09-30minor changes to arithmetic assertions involving nonlinearity and models ↵Morgan Deters
(related to bug 405)
2012-09-30minor fixes to pickler (hopefully fixes Debian build from last night)Morgan Deters
2012-09-30release notesMorgan Deters
2012-09-29Calling the setIncompleteness() flag on all full checks once a non-linear ↵Tim King
term has been seen.
2012-09-29Fix a few segfaults in driver.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-29draft RELEASE-NOTES file, and minor release stuffMorgan Deters
2012-09-29fixes to "make distclean" and C compatibility bindings; should fix the ↵Morgan Deters
broken builds last night
2012-09-29fixes to "make distclean" and C compatibility bindings; should fix the ↵Morgan Deters
broken builds last night
2012-09-29This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and ↵Tim King
DIVISION. Improves support for non-linear monomials in getEqualityStatus(). Fixes bug 405.
2012-09-28Some fixes to portfolioKshitij Bansal
* 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.)
2012-09-28fix distribution of cvc4_assert.iMorgan Deters
2012-09-28fixes for compatibility (i.e., CVC3) Java bindingsMorgan Deters
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to ↵Morgan Deters
make it unambiguous for case-insensitive filesystems like on Mac. Fixes Mac builds
2012-09-28some fixes to build systemMorgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-28fix production-build linking errorMorgan Deters
2012-09-28Public interface review items:Morgan Deters
* 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.
2012-09-28* fix compatibility library naming for SMT-LIBv1Morgan Deters
* 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.)
2012-09-27* Rename SMT parts (printer, parser) to SMT1Morgan Deters
* 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.)
2012-09-27finally, a portable solutionMorgan Deters
2012-09-27fix for non-MacMorgan Deters
2012-09-27speed up mkoptions script (esp. on Macs)Morgan Deters
2012-09-27better progress indicator for mkoptionsMorgan Deters
2012-09-26disable building of cvc3_george system-test object (which isn't used yet ↵Morgan Deters
anyway, and required ~10 minutes to build with -O3). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-26Finish off SEXPR kind work.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-26updates to model generation : do not modify equality engine during getValue, ↵Andrew Reynolds
other minor changes, still problems with constants not being specified for some eq classes
2012-09-26Fix a handful of things for Mac, and Java bindings.Morgan Deters
Also add a "mac-build" script that sets up prerequisites for Mac.
2012-09-26bug #398 test (bug was resolved last night), and a script to download all ↵Morgan Deters
bug attachments from bugzilla and put them in the tree
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback