Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |||
2012-11-30 | Changing the documentation of ARR_TABLE_FUN to say (internal symbol). | Tim King | |
2012-11-30 | quantifiers now uses master equality engine, preparation work to cleanup code | Andrew Reynolds | |
2012-11-26 | Adding support for a master equality engine. Each theory gets the master ↵ | Dejan Jovanović | |
equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit(). | |||
2012-11-17 | Fixed last currently known bug in array models | Clark Barrett | |