summaryrefslogtreecommitdiff
path: root/src/theory/valuation.cpp
AgeCommit message (Collapse)Author
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2014-10-16Add dt.size to datatypes theory. Add option for fairness strategy used by ↵ajreynol
CEGQI. Improve care graph/equality status for datatypes. Only do FULL effort check in datatypes if no other theories used output channel.
2014-10-02Better getEqualityStatus for arrays, smarter combination of theoriesClark Barrett
2014-05-05Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and ↵Morgan Deters
contract is the same as for TheoryEngine version.
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-26addingDejan Jovanović
* getModelValue to valuation * getModelValue to theory engine * getModelValue to theory implemented getModelValue in bitvector the purpose of getModelValue is to ask for a concrete value of a shared term
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-31merge from fmf-devel branch. more updates to models: now with ↵Andrew Reynolds
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and ↵Andrew Reynolds
(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
This should also fix bug 325.
2012-04-11merge from arrays-clark branchMorgan Deters
2011-10-17Sharing workDejan Jovanović
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update ↵Morgan Deters
to model gen on booleans; and a little cleanup
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-09surprize surprizeDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
2011-04-07Made Valuation::getValue() and Valuation::getSatValue() const.Tim King
2011-03-31Fixes to Valuation.Tim King
2011-03-30Add Valuation::getSatValue() so that theories can access the currentMorgan Deters
(propositional) assignment for theory atoms. Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list. This implementation leads to some compiler warnings in production builds, but these will be corrected in coming days. There appears to be a small speedup in the parser as a result of this fix: http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5 Cleaned up a few CD Boolean attribute things. Various small fixes to coding guidelines / test coverage. This commit: * Resolves bug 252 (tracing not disabled in production builds) * Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())
2011-02-26Merge from theory-break-dependences branch to break Theory and TheoryEngine ↵Morgan Deters
dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine. If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use).
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback