summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-10-23Fixed inefficiency in bit-vector rewrite rule.lianah
2014-10-22Fix bug590 regression distcheck failure from last night.Morgan Deters
2014-10-21Fixed bug 589Tianyi Liang
2014-10-21Fixed bug 590, added regression testClark Barrett
2014-10-20Minor cleanup in datatypes.ajreynol
2014-10-19Merge pull request #59 from kbansal/sets3Kshitij Bansal
sets type enumerator
2014-10-19Finish sets type enumerator implementation.Kshitij Bansal
2014-10-19fix statistic in decision engineKshitij Bansal
2014-10-18Fix assertion.ajreynol
2014-10-18Add dt lemma: zero size implies nullary constructor.ajreynol
2014-10-18Fix for bounded integers when incremental, fixes bug 588. Add option ↵ajreynol
--dt-binary-split.
2014-10-17Merge branch '1.4.x'Morgan Deters
2014-10-17Remove a bad (unstable, timing-dependent) test.Morgan Deters
2014-10-17Minor change for performance according to Andy's suggestion.Tianyi Liang
2014-10-16Fix clang warningsMorgan Deters
2014-10-16Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ↵ajreynol
changes to options.
2014-10-16Merge branch '1.4.x'Morgan Deters
2014-10-16Add Thomas Hunger to THANKS file (for having submitted patches).Morgan Deters
2014-10-16Use n-ary splits instead of binary splits in theory datatypes.ajreynol
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-14fix for memory leak in BVQuickChecklianah
2014-10-14Merge pull request #58 from mdeters/smt-attributesMorgan Deters
Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.
2014-10-14Context-dependent expr attributes are now attached to a specific SmtEngine, ↵Morgan Deters
and the SAT context is owned by the SmtEngine.
2014-10-14amend prvs commitKshitij Bansal
2014-10-14trace decision-nodeKshitij Bansal
2014-10-13CEGQI uses model. Enforce fairness in CEGQI natively.ajreynol
2014-10-13Model building into quantifiers engine. Simplify axiom-inst mode.ajreynol
2014-10-13Refactor model builder from model engine to quant engine. Work on fairness ↵ajreynol
strategy for CEGQI. Add option for single/multi triggers. Minor cleanup.
2014-10-11Merge branch '1.4.x'Morgan Deters
2014-10-11Some defensive programming at destruction time, and fix a latent dangling ↵Morgan Deters
pointer bug.
2014-10-10Merge remote-tracking branch 'origin/1.4.x'Kshitij Bansal
2014-10-10Initial draft of CEGQI.ajreynol
2014-10-10Fix issue with shared but non-preregistered term setup. Thanks Alvise ↵Kshitij Bansal
Rabitti for the report.
2014-10-10CleanupMorgan Deters
2014-10-10Add owner map to better manage QuantifiersModules. Initial infrastructure ↵ajreynol
for cegqi.
2014-10-09Refactor quantifier prenex option. By default, do not pull quantifiers with ↵ajreynol
user patterns.
2014-10-08Merge branch '1.4.x'Morgan Deters
2014-10-08Add unsat cores support to CVC native language.Morgan Deters
2014-10-08Some minor cleanup.Morgan Deters
2014-10-08Remove private header from public driver.Morgan Deters
2014-10-07Fix portoflio issues (debugging code was being called even when tag was off)Kshitij Bansal
2014-10-07Merge remote-tracking branch 'upstream/master' into sets-mergableKshitij Bansal
2014-10-07update default Sets optionsKshitij Bansal
2014-10-07whitespace fixesKshitij Bansal
2014-10-08Cache for getInstance, thanks to Johannes Kanig for the report. Do not ↵ajreynol
mkRep for multi triggers.
2014-10-07add couple of statsKshitij Bansal
2014-10-07sets stronger equality propagatorKshitij Bansal
2014-10-07Refactor quantifiers attributes.ajreynol
2014-10-07define-const is an extended command, not permitted in strict mode.Morgan Deters
2014-10-06Fix unit test that was broken with last commit.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback