summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2013-03-26moving bv before arraysDejan Jovanović
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-21another typo/bugfix for equality constant evaluationDejan Jovanović
2013-03-21Better error in case of nonlinear assertions while in linear logicMorgan Deters
2013-03-21fixing markings of internal nodes in equality engineDejan Jovanović
2013-03-21more equality constant evaluationDejan Jovanović
2013-03-21fixing constant evaluation bugsDejan Jovanović
2013-03-19Adding evaluation of constant terms to the equality engine. Evaluation on a ↵Dejan Jovanović
particular kind can be set by setting interpreted = true when calling addFunctionKind.
2013-03-19Minor cleanup of sourcesMorgan Deters
2013-03-15changed default option for quantifier instantiationAndrew Reynolds
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds ↵Morgan Deters
and src
2013-03-13Added a rewrite for iff:Clark Barrett
x = c iff x = d ---> false This fixes Andy's problem if unconstrained simplification is turned on.
2013-03-11ite removal option for quantifiers --ite-remove-quant, e-matching for ↵Andrew Reynolds
boolean terms, improvement for pre skolemization
2013-03-06Best heuristics for handling decision requests from arraysClark Barrett
2013-03-06fixed two bugs for the new E-matching implementation, added aggressive ↵Andrew Reynolds
miniscoping option --ag-miniscope-quant, minor cleanup
2013-02-26Bug fix for rep-set.Morgan Deters
(Cherry-picked from commit c71ec27 in master.)
2013-02-26Merge branch '1.0.x'lianah
2013-02-26Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.xlianah
2013-02-26fix for bv crash in incremental mode; this is a temporary fix for bug 493lianah
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as ↵Andrew Reynolds
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-15Merge branch '1.0.x'Tim King
2013-02-15repairs a bug in rewriterule engine: constructor cannot be used as a patternTianyi Liang
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc) Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-02-14Removing BVDebug and replacing with Debug.Tim King
2013-02-13repairs a bug in rewriterule engine: constructor cannot be used as a patternTianyi Liang
2013-02-12Fix a preprocessing performance issue.Morgan Deters
2013-02-07Merge branch '1.0.x'Morgan Deters
Conflicts: src/theory/quantifiers/theory_quantifiers.cpp
2013-02-07Only put quantifier assertions in model equality engine if fullModel==trueMorgan Deters
2013-02-07Significant work on bug #491 (not yet closed).Morgan Deters
2013-02-07More complete fix for bug 484 (includes fixes for records and tuples).Morgan Deters
2013-02-07Fix error in tuple type-checking.Morgan Deters
2013-02-06make datatypes enumerator behavior clearer (no exceptions in normal operation)Morgan Deters
2013-02-06make datatypes enumerator behavior clearer (no exceptions in normal operation)Morgan Deters
2013-02-05dos2unix conversion for a number of files; this avoids spurious conflicts ↵Morgan Deters
when merging to master
2013-02-05More improvements for E-matchingAndrew Reynolds
2013-02-04fixed files with DOS newlines; fixed contrib/ scripts to use gitMorgan Deters
2013-02-04Some fixes for the miplib preprocessing pass.Morgan Deters
* TNode violation bug fix (thanks to Tim King for discovery & fix) * change Boolean miplib-trick substitution option into a threshold * ppAssert() the generated miplib constraints to arithmetic
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed ↵Morgan Deters
bug 492 and resolves previous issue for bug 486. (cherry picked from *part* of commit e54c0f73712b25f1d6d49a3817c923eea077da81) Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed ↵Andrew Reynolds
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
2013-02-03Some cleanup of miplib regressions and optionsMorgan Deters
2013-02-03new option for doing top-level miplib substitutions (or not)Morgan Deters
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-02-03Remove old miplibtrick from arith static learnerMorgan Deters
2013-01-31Adding a heuristic to more eagerly split bounded integer variables.Tim King
2013-01-28fix for finite model finding caused by new collectModelInfo codeAndrew Reynolds
2013-01-28made QuantifiersEngine::d_inst_match_trie and ↵Andrew Reynolds
QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486 (cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)
2013-01-28made QuantifiersEngine::d_inst_match_trie and ↵Andrew Reynolds
QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
2013-01-27some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵Andrew Reynolds
datatypes theory still crashes for datatypes with boolean subfields (cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)
2013-01-27some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵Andrew Reynolds
datatypes theory still crashes for datatypes with boolean subfields
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback