summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2012-10-06* Clean up some options documentationMorgan Deters
* Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-06* Some documentation about building compatibility and language bindingsMorgan Deters
* Better errors/warnings when SWIG isn't installed (resolves bug 373) * Allow compatibility bindings to be built when SWIG isn't available
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-03New model code, mostly workinClark Barrett
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-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-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-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-26Fix type checking for define-funs (resolves bug 398).Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-26The Tuesday Afternoon Catch-All Commit (TACAC):Morgan Deters
* --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.)
2012-09-25fix some Mac issuesMorgan Deters
2012-09-25some buggy examples for incrementality, and make bug326 run as part of make ↵Morgan Deters
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.)
2012-09-24some api changesDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback