Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-03-21 | fixing markings of internal nodes in equality engine | Dejan Jovanović | |
2013-03-21 | more equality constant evaluation | Dejan Jovanović | |
2013-03-21 | fixing constant evaluation bugs | Dejan Jovanović | |
2013-03-19 | Adding 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-19 | Minor cleanup of sources | Morgan Deters | |
2013-03-15 | changed default option for quantifier instantiation | Andrew Reynolds | |
2013-03-14 | Merge branch '1.0.x' | Morgan Deters | |
2013-03-14 | fix to build system: #include the proper file when they are in both builds ↵ | Morgan Deters | |
and src | |||
2013-03-13 | Added 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-11 | ite removal option for quantifiers --ite-remove-quant, e-matching for ↵ | Andrew Reynolds | |
boolean terms, improvement for pre skolemization | |||
2013-03-06 | Best heuristics for handling decision requests from arrays | Clark Barrett | |
2013-03-06 | fixed two bugs for the new E-matching implementation, added aggressive ↵ | Andrew Reynolds | |
miniscoping option --ag-miniscope-quant, minor cleanup | |||
2013-02-26 | Bug fix for rep-set. | Morgan Deters | |
(Cherry-picked from commit c71ec27 in master.) | |||
2013-02-26 | Merge branch '1.0.x' | lianah | |
2013-02-26 | Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x | lianah | |
2013-02-26 | fix for bv crash in incremental mode; this is a temporary fix for bug 493 | lianah | |
2013-02-24 | added 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-16 | Some cleanup and copyright updating | Morgan Deters | |
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles | |||
2013-02-15 | Merge branch '1.0.x' | Tim King | |
2013-02-15 | repairs a bug in rewriterule engine: constructor cannot be used as a pattern | Tianyi Liang | |
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc) Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2013-02-14 | Removing BVDebug and replacing with Debug. | Tim King | |
2013-02-13 | repairs a bug in rewriterule engine: constructor cannot be used as a pattern | Tianyi Liang | |
2013-02-12 | Fix a preprocessing performance issue. | Morgan Deters | |
2013-02-07 | Merge branch '1.0.x' | Morgan Deters | |
Conflicts: src/theory/quantifiers/theory_quantifiers.cpp | |||
2013-02-07 | Only put quantifier assertions in model equality engine if fullModel==true | Morgan Deters | |
2013-02-07 | Significant work on bug #491 (not yet closed). | Morgan Deters | |
2013-02-07 | More complete fix for bug 484 (includes fixes for records and tuples). | Morgan Deters | |
2013-02-07 | Fix error in tuple type-checking. | Morgan Deters | |
2013-02-06 | make datatypes enumerator behavior clearer (no exceptions in normal operation) | Morgan Deters | |
2013-02-06 | make datatypes enumerator behavior clearer (no exceptions in normal operation) | Morgan Deters | |
2013-02-05 | dos2unix conversion for a number of files; this avoids spurious conflicts ↵ | Morgan Deters | |
when merging to master | |||
2013-02-05 | More improvements for E-matching | Andrew Reynolds | |
2013-02-04 | fixed files with DOS newlines; fixed contrib/ scripts to use git | Morgan Deters | |
2013-02-04 | Some 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-04 | Model 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-04 | Model 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-03 | Some cleanup of miplib regressions and options | Morgan Deters | |
2013-02-03 | new option for doing top-level miplib substitutions (or not) | Morgan Deters | |
2013-02-03 | new miplib pass, works for 1 or 2 vars | Morgan Deters | |
2013-02-03 | Remove old miplibtrick from arith static learner | Morgan Deters | |
2013-01-31 | Adding a heuristic to more eagerly split bounded integer variables. | Tim King | |
2013-01-28 | fix for finite model finding caused by new collectModelInfo code | Andrew Reynolds | |
2013-01-28 | made 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-28 | made QuantifiersEngine::d_inst_match_trie and ↵ | Andrew Reynolds | |
QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486 | |||
2013-01-27 | some 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-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵ | Andrew Reynolds | |
datatypes theory still crashes for datatypes with boolean subfields | |||
2013-01-26 | Merge branch '1.0.x' | Morgan Deters | |
2013-01-26 | another fix for quantifier models (related to bug 486) | Morgan Deters | |
2013-01-25 | fix --check-model --finite-model-find when used together (related to bug 486) | Morgan Deters | |
2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters | |