summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2012-10-09usability: remove --no-interactive from --smtlib optionMorgan Deters
2012-10-09fix for bug 415Dejan Jovanović
2012-10-09* Add assertion in TheoryModel code to ensure we don't get inconsistentMorgan Deters
substitutions for solved variables. Related to bug 418 (and might resolve it). * Respect phase-locking in Minisat (one phase-saving site was unguarded). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09fix beta reduction in both preRewrite() *and* postRewrite(), related to bug ↵Morgan Deters
417. oops. also fix spelling on "rewritting" test
2012-10-09some documentation fixesMorgan Deters
2012-10-09adding mergePredicates method to the equality engine to be able toDejan Jovanović
assert equalities betweeen predicates
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
(rather than SAT context) * Enable part of CVC3 system test (resolves bug 375) * Fix infinite recursion in beta reduction code (resolves bug 417) * Some model-building assertions have been added * Other minor changes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-08Fixed problem in assertEqualityEngine: predicates that are not false are noClark Barrett
longer assumed to be true
2012-10-08small fix for compat JNI library installationMorgan Deters
2012-10-08fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't ↵Morgan Deters
allow use of any BV ops
2012-10-06* more complete support for --dump assertions:{pre,post}-PREPROCESSING-PASSMorgan Deters
* more minor cleanup/doc (this commit was certified error- and warning-free by the test-and-commit script.)
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback