summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2014-10-14fix for memory leak in BVQuickChecklianah
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-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-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-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-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-06Fix a resource limiting issue where interruption didn't occur promptly. ↵Morgan Deters
Thanks Johannes Kanig for the report.
2014-10-06Some minor cleanup.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06fix for bug586Kshitij Bansal
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-10-02fix getModelValue(<non-preregistered term>)Kshitij Bansal
2014-10-01Option for more aggressive merging in UEE.ajreynol
2014-09-30Proofs- and cores-related segfault fixes (mainly a usability issue), thanks ↵Morgan Deters
Christoph Sticksel for reporting these.
2014-09-29Add option for aggressive model filtering in conjecture generator (enumerate ↵ajreynol
ground terms).
2014-09-27Merge branch '1.4.x'Morgan Deters
2014-09-27Fix infinite loop in --bitblast-aig/--bv-aig-simp options.Morgan Deters
2014-09-26Merge branch '1.4.x'Morgan Deters
2014-09-26Fix bv options doc.Morgan Deters
2014-09-26Finer-grained resource-limiting in quantifiers.Morgan Deters
2014-09-26Fix AIG bitblaster for unsat cores.Morgan Deters
2014-09-25Fair datatype enumeration.ajreynol
2014-09-24Fix infinite loop in datatypes enumerator. Minor work on conjecture generator.ajreynol
2014-09-24Refactor option for uf+cardinality constraints solver.ajreynol
2014-09-24Partial support for codatatype models.ajreynol
2014-09-23Support :no-pattern.ajreynol
2014-09-23Do not throw error when codatatype is not well-founded. Add option for ↵ajreynol
disabling codatatype reasoning. Minor cleanup.
2014-09-18Resource spending support in theories (and especially in quantifiers).Morgan Deters
2014-09-17Fix soundness bug for quantifier macros involving Int/Real.ajreynol
2014-09-17Refactor entailment filtering for conjecture generator. Other minor cleanup.ajreynol
2014-09-17More refactoring of conjecture generation. Term generation into own class.ajreynol
2014-09-16Bug fix variable triggers with --inst-max-level : use term in EQC with ↵ajreynol
minimal instantiation level.
2014-09-16Refactoring of conjecture generator. Determine subgoals are non-canonical ↵ajreynol
based on ground equalities. Add filtering options to options file.
2014-09-09Fix bug for variable term triggers within multi-triggers.ajreynol
2014-09-09Accept user-provided triggers with variable terms. Flush lemmas before ↵ajreynol
quantifiers check. Minor fix for conjecture generation.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback