summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-10-11Fix wording on GPL in legal notices; also remove an unnecessary source ↵Morgan Deters
dependence. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-11compliance noteMorgan Deters
2012-10-10Abstract values for SMT-LIB.Morgan Deters
Also fix bug 421 relating to incrementality and models. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-10cleanup up some static data members in the quantifiers codeAndrew Reynolds
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-10-09typoKshitij Bansal
2012-10-09bugfix: isQuantified, bugfix: flushKshitij Bansal
2012-10-09fixed datatypes rewriter to detect clashes between non-datatype subfields. ↵Andrew Reynolds
cleaned up model code, TheoryModel::getValue is now const.
2012-10-09* make Model class private (as discussed at meeting today)Morgan Deters
* fix minor issue with s-expr parsing in CVC and SMT grammars * other minor things (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09fixed bv rewriter to evaluate bvurem over constantsLiana Hadarean
2012-10-09More fixes to model codeClark Barrett
2012-10-09made datatypes rewrite incorrect selectors to ground term. this feature can ↵Andrew Reynolds
be turned off by --disable-dt-rewrite-error-sel. changed regression answer to reflect new default behavior.
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-08added reduced bv model failing test caseLiana Hadarean
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-06turn off cudd by default in configure scriptMorgan Deters
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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback