summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2012-10-24efficient e-matching now specific to rewrite rulesAndrew Reynolds
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific cod...Andrew Reynolds
2012-10-23fixed problem with datatypes giving incorrect explanations, now corrected and...Andrew Reynolds
2012-10-23More debugging info, small changes to model builderClark Barrett
2012-10-23Added reads that were missing in collectModelInfoClark Barrett
2012-10-23fixed TheoryBV collectModel info to check for shared terms; this seems to fix...Liana Hadarean
2012-10-23more updates to inst gen: fixed partial instantiations, recognize duplicate d...Andrew Reynolds
2012-10-19Fix for model building with shared terms for arithmetic.Tim King
2012-10-19BV theory model fixLiana Hadarean
2012-10-19--fallback-sequential / --no-fallback-sequential optionKshitij Bansal
2012-10-17first working version of new inst-gen-style quantifier instantiation techniqu...Andrew Reynolds
2012-10-16more cleanup of quantifiers codeAndrew Reynolds
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of quantif...Andrew Reynolds
2012-10-14fix #line number warnings (sorry!)Morgan Deters
2012-10-12Added assertions and tracing code for collectModelInfo phaseClark Barrett
2012-10-12Latest changes to model codeClark Barrett
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-10Abstract values for SMT-LIB.Morgan Deters
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-09fixed datatypes rewriter to detect clashes between non-datatype subfields. c...Andrew Reynolds
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
2012-10-09fix for bug 415Dejan Jovanović
2012-10-09* Add assertion in TheoryModel code to ensure we don't get inconsistentMorgan Deters
2012-10-09fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 4...Morgan Deters
2012-10-09adding mergePredicates method to the equality engine to be able toDejan Jovanović
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
2012-10-08Fixed problem in assertEqualityEngine: predicates that are not false are noClark Barrett
2012-10-06* Clean up some options documentationMorgan Deters
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
2012-10-05fix \fileMorgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-04disable model-generation by default in cvc3 compatibility layer. should fix ...Morgan Deters
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
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-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
2012-10-02* re-enable some Z3 extended commands:Morgan Deters
2012-10-01make sure to mark LogicInfo as CVC4_PUBLICMorgan Deters
2012-10-01initial draft of skolemization during pre-processing, made simple cliques the...Andrew Reynolds
2012-09-30minor changes to arithmetic assertions involving nonlinearity and models (rel...Morgan Deters
2012-09-29Calling the setIncompleteness() flag on all full checks once a non-linear ter...Tim King
2012-09-29This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and ...Tim King
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-28Public interface review items:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback