summaryrefslogtreecommitdiff
path: root/src/theory/arrays
AgeCommit message (Collapse)Author
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2015-03-25change const are triggers from false to true in equality enginesKshitij Bansal
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan 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-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-10-30Be more lazy about generating array lemmasClark Barrett
2014-10-29Added new, much faster, care graph computation for arraysClark Barrett
Force split on true first in combineTheories Fix bugs in getModelValue in bit-vectors
2014-10-21Fixed bug 590, added regression testClark Barrett
2014-10-02Added internal support for constant arrays.Clark Barrett
2014-10-02Added option for developer use onlyClark Barrett
2014-10-02More model-based combination for arraysClark Barrett
2014-10-02Better getEqualityStatus for arrays, smarter combination of theoriesClark Barrett
2014-07-12Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre ↵Morgan Deters
for the report.
2014-07-01Update copyrights.Morgan Deters
2014-06-27Fix for bug543Clark Barrett
2014-06-21Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, ↵Morgan Deters
and arith.
2014-05-26Fixing Tim's subtype/solving bug for arraysClark Barrett
2014-04-17simplify 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-14Add ability to provide theory-specific proof rules to EqualityEngine, ↵Andrew Reynolds
extends enumeration of MergeReasonType. Add initial use in TheoryArrays.
2014-02-21add 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-22Delay QuantifiersEngine and UF strong solver initialization until after ↵Morgan Deters
final options/logic are set.
2013-11-27General pre-release cleanup commitMorgan 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-25Array collectModelInfo fix for AndyClark Barrett
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-06-07Fix for bug 517.Morgan Deters
2013-05-23Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.Andrew Reynolds
2013-05-08Fixed assertion bugClark Barrett
2013-05-07fix for nonterminating model-based array loopMorgan Deters
2013-05-06Some bug fixes for mb arraysClark Barrett
2013-05-02* splitLemma to request atomsDejan Jovanović
* normalizing in bv before bitblasting
2013-04-11Improved speed of no redundant lemma assertion by using hash setClark Barrett
2013-04-11Added check for infinite lemma loopClark Barrett
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Made eager lemmas an option, enabled for QF_AXClark Barrett
2013-03-30Disabling eager array index splitting for QF_AUFLIAClark Barrett
Minor changes to model-based array solver
2013-03-28fix memory corruption in arrays destructorMorgan Deters
2013-03-27Fixed a warning, made eager-index default to true (better for QF_AUFBV)Clark Barrett
2013-03-27Fixed bug in arraysClark Barrett
2013-03-27Updates to model-based array solverClark Barrett
Minor fixes to bv and theory_engine
2013-03-27New model-based array procedureClark Barrett
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-06Best heuristics for handling decision requests from arraysClark Barrett
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-05dos2unix conversion for a number of files; this avoids spurious conflicts ↵Morgan Deters
when merging to master
2013-02-04fixed files with DOS newlines; fixed contrib/ scripts to use gitMorgan Deters
2012-12-05This 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-01Throw a logic exception if user makes an assertion using a STORE_ALLClark Barrett
2012-12-01drastic 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback