summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
AgeCommit message (Collapse)Author
2015-05-29changed resource step options to unsignedlianah
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2015-05-15Avoid ensureLiteral on unpreprocessed formulas in cbqi.ajreynol
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-02-22New trigger options. --inst-no-entail on by default. Misc cleanup.ajreynol
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor ↵ajreynol
refactor of previous commit.
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-12-03Revert "Disable constants sharing in eq engine, disable hack in theory engine."Kshitij Bansal
This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba. In particular, it DOES NOT revert "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine." which is part of the same commit.
2014-11-20Disable constants sharing in eq engine, disable hack in theory engine. ↵ajreynol
Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
2014-11-18Set Constant's normal form and other short fixesKshitij Bansal
Other short fixes: * use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT * theoryof-mode fix in smt_engine.cpp * hack in TheoryModel::getModelValue [TODO: notify Clark/Andy] * Lemma generation when it rewrites to true/false fix * TermInfoManager::addTerm(..) fix * Move SUBSET rewrite to preRewrite * On preRegister, queue up propagation to be done upfront ** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code. * TheorySetsProperties::getCardinality(..) fix Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing!
2014-11-17Resource-limiting work.Liana Hadarean
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-11-10Do not eliminate variables only occurring in patterns. Minor improvements ↵ajreynol
to sort inference. Remove unused code.
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-02Added internal support for constant arrays.Clark Barrett
2014-10-02More model-based combination for arraysClark Barrett
2014-10-02Better getEqualityStatus for arrays, smarter combination of theoriesClark Barrett
2014-09-30Proofs- and cores-related segfault fixes (mainly a usability issue), thanks ↵Morgan Deters
Christoph Sticksel for reporting these.
2014-09-18Resource spending support in theories (and especially in quantifiers).Morgan Deters
2014-08-24improvements to sets sharingKshitij Bansal
* Add TheorySets::getEqualityStatus(TNode, TNode) * Add TheorySets::getModelValue(TNode)
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-18Add support for quantifier-specific instantiation levels. Add option for ↵ajreynol
setting inst-level 0 only for input terms.
2014-07-01Update copyrights.Morgan Deters
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ↵Andrew Reynolds
assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
2014-04-30T-entailment work, and QCF (quant conflict find) work that uses it.Tim King
This commit includes work from the past month on the T-entailment check infrastructure (due to Tim), an entailment check for arithmetic (also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds). Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-03-11Fix for rewriterules build breakage.Morgan Deters
2014-03-11Initial refactor of rewrite rules, make theory_rewriterules empty theory. ↵Andrew Reynolds
Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter. Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up. QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master. Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern. Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE. Merging rewrite rules into master, check-model current fails on 3 FMF regressions. Fix check-model issue, a line of code was omitted during merge.
2014-03-08Fixing name changes that cam in from the merge.Tim King
2014-03-07Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into ↵Tim King
master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
2014-03-06adds incremental for strings; clean-up codesTianyi Liang
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵Morgan Deters
(resolves bug #548).
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.
2014-01-18strings with new ideasTianyi Liang
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified ↵Andrew Reynolds
formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof ↵Morgan Deters
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
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-25Substantial Changes:Tim King
-ITE Simplification -- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities. -- Separated simpWithCare from simpITE. -- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants. -- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically. -- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks. -- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches. - TheoryEngine -- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above. -- Switched UnconstrainedSimplifier to a pointer. - RemoveITEs -- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. - Theory Bool Rewriter -- Added additional simplifications for boolean ites. Minor Changes: - TheoryModel -- Removed vestigial copy of the ITESimplifier. - AttributeManager -- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. -NodeManager -- Added additional functions for reclaiming zombies. -- Exposed the size of the node pool for heuristics that worry about memory consumption. - NaryBuilder -- Added convenience classes for constructing associative and commutative n-ary operators. -- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
2013-10-07fixed some bugsLiana Hadarean
2013-09-27Some fixes to recent strings commits.Morgan Deters
2013-09-27adds model generation for strings, and a hacked way in arith engine for modelsTianyi Liang
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-05Fix bugs/issues with missed-t-prop dump outputMorgan Deters
2013-06-27Better check-models output for some kinds of problems; add anassertion that ↵Morgan Deters
the master equality engine is consistent when it needs to be. This is intended to help root out some recent model-generation bugs.
2013-05-21Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵Morgan Deters
to improper ITE removal in quantifier instantiations.
2013-05-20disable Logic-checking with finite model finding for now, since FMF uses ↵Morgan Deters
Rationals, making the check think arithmetic should be enabled (but it's not)
2013-05-20Fix erroneous results when the logic was incorrectly specified (by throwing ↵Morgan Deters
LogicException). Also correct a case where sharing was doing some work during pure theory solving.
2013-05-07fix for bug500Dejan Jovanović
2013-05-02* splitLemma to request atomsDejan Jovanović
* normalizing in bv before bitblasting
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback