Age | Commit message (Collapse) | Author | |
---|---|---|---|
2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean | |
2015-03-25 | change const are triggers from false to true in equality engines | Kshitij Bansal | |
2014-12-26 | Adding an option to the equality engine constructor to treat all constants as | Dejan Jovanovic | |
trigger terms. I've disabled constants as triggers for all equality engines except for the shared terms engine where it is needed. | |||
2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters | |
2014-10-30 | Be more lazy about generating array lemmas | Clark Barrett | |
2014-10-29 | Added new, much faster, care graph computation for arrays | Clark Barrett | |
Force split on true first in combineTheories Fix bugs in getModelValue in bit-vectors | |||
2014-10-21 | Fixed bug 590, added regression test | Clark Barrett | |
2014-10-02 | Added internal support for constant arrays. | Clark Barrett | |
2014-10-02 | Added option for developer use only | Clark Barrett | |
2014-10-02 | More model-based combination for arrays | Clark Barrett | |
2014-10-02 | Better getEqualityStatus for arrays, smarter combination of theories | Clark Barrett | |
2014-07-12 | Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre ↵ | Morgan Deters | |
for the report. | |||
2014-07-01 | Update copyrights. | Morgan Deters | |
2014-06-27 | Fix for bug543 | Clark Barrett | |
2014-06-21 | Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, ↵ | Morgan Deters | |
and arith. | |||
2014-05-26 | Fixing Tim's subtype/solving bug for arrays | Clark Barrett | |
2014-04-17 | simplify mkSkolem naming system: don't use $$ | Kshitij Bansal | |
Short summary: By default NODEID is appeneded, just continue doing what you were, just don't add the _$$ at the end. Long summary: Before this commit there were four (yes!) ways to specify the names for new skolems, which result in names as given below 1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 2) mkSkolem("name", ..., SKOLEM_EXACT_NAME) -> "name" 3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me" After this commit, only 1) and 2) stay. 90% usage is of 1) or 3), which results in exact same behavior (and looking at the source code it doesn't look like everyone realized that the _$$ is just redundant). Almost no one used 4), which is the only reason to even have $$. Post this commit if you really want a number in the middle, manually construct the name and use the SKOLEM_EXACT_NAME flag. | |||
2014-03-14 | Add ability to provide theory-specific proof rules to EqualityEngine, ↵ | Andrew Reynolds | |
extends enumeration of MergeReasonType. Add initial use in TheoryArrays. | |||
2014-02-21 | add new theory (sets) | Kshitij Bansal | |
Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment | |||
2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after ↵ | Morgan Deters | |
final options/logic are set. | |||
2013-11-27 | General pre-release cleanup commit | Morgan Deters | |
* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing | |||
2013-11-25 | Array collectModelInfo fix for Andy | Clark Barrett | |
2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters | |
2013-06-07 | Fix for bug 517. | Morgan Deters | |
2013-05-23 | Refactoring to prepare for MBQI with integer quantification. Minor bug fixes. | Andrew Reynolds | |
2013-05-08 | Fixed assertion bug | Clark Barrett | |
2013-05-07 | fix for nonterminating model-based array loop | Morgan Deters | |
2013-05-06 | Some bug fixes for mb arrays | Clark Barrett | |
2013-05-02 | * splitLemma to request atoms | Dejan Jovanović | |
* normalizing in bv before bitblasting | |||
2013-04-11 | Improved speed of no redundant lemma assertion by using hash set | Clark Barrett | |
2013-04-11 | Added check for infinite lemma loop | Clark Barrett | |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-01 | update copyrights | Morgan Deters | |
2013-04-01 | Made eager lemmas an option, enabled for QF_AX | Clark Barrett | |
2013-03-30 | Disabling eager array index splitting for QF_AUFLIA | Clark Barrett | |
Minor changes to model-based array solver | |||
2013-03-28 | fix memory corruption in arrays destructor | Morgan Deters | |
2013-03-27 | Fixed a warning, made eager-index default to true (better for QF_AUFBV) | Clark Barrett | |
2013-03-27 | Fixed bug in arrays | Clark Barrett | |
2013-03-27 | Updates to model-based array solver | Clark Barrett | |
Minor fixes to bv and theory_engine | |||
2013-03-27 | New model-based array procedure | Clark Barrett | |
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-06 | Best heuristics for handling decision requests from arrays | Clark Barrett | |
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-05 | dos2unix conversion for a number of files; this avoids spurious conflicts ↵ | Morgan Deters | |
when merging to master | |||
2013-02-04 | fixed files with DOS newlines; fixed contrib/ scripts to use git | Morgan Deters | |
2012-12-05 | This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ↵ | Tim King | |
CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap. | |||
2012-12-01 | Throw a logic exception if user makes an assertion using a STORE_ALL | Clark Barrett | |
2012-12-01 | drastic simplification of quantifiers code regarding equality queries, ↵ | Andrew Reynolds | |
instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine |