summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.cpp
AgeCommit message (Expand)Author
2015-02-04Refactor sygus_util to TermDb. Initial work on solution reconstruction into ...ajreynol
2015-01-29Restrict LtePartialInst instantiations based on E-matching, promote to quanti...ajreynol
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor refactor...ajreynol
2015-01-24Variable patterns only look at eligible terms. Minor refactoring of quantifi...ajreynol
2015-01-24Add --lte-restrict-inst-closure option. Push dt.size fairness constraints in...ajreynol
2015-01-23Rework inst-closure.ajreynol
2015-01-22Add option --lte-partial-inst. Remove inst-closure.ajreynol
2014-11-28Synchronize conjecture generation with E-matching. Minor fix to --full-satur...ajreynol
2014-11-25Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos...ajreynol
2014-11-20Disable constants sharing in eq engine, disable hack in theory engine. Chang...ajreynol
2014-11-18Compute model basis only for fmf. Add another co-datatype regression.ajreynol
2014-11-13Remove two obsolete versions of MBQI.ajreynol
2014-11-07Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor impr...ajreynol
2014-11-07Properly distinguish which EQC to assign values in datatypes, use assertRepre...ajreynol
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 s...ajreynol
2014-10-10Initial draft of CEGQI.ajreynol
2014-10-10Add owner map to better manage QuantifiersModules. Initial infrastructure fo...ajreynol
2014-10-08Cache for getInstance, thanks to Johannes Kanig for the report. Do not mkRep...ajreynol
2014-10-07Refactor quantifiers attributes.ajreynol
2014-10-06Fix a resource limiting issue where interruption didn't occur promptly. Than...Morgan Deters
2014-09-26Finer-grained resource-limiting in quantifiers.Morgan Deters
2014-09-24Refactor option for uf+cardinality constraints solver.ajreynol
2014-09-23Do not throw error when codatatype is not well-founded. Add option for disab...ajreynol
2014-09-18Resource spending support in theories (and especially in quantifiers).Morgan Deters
2014-09-16Bug fix variable triggers with --inst-max-level : use term in EQC with minima...ajreynol
2014-09-09Accept user-provided triggers with variable terms. Flush lemmas before quant...ajreynol
2014-08-29Set instantiation level on skolemized bodies of quantifiers. Rename inst-lev...ajreynol
2014-08-26Bug fixes for --purify-triggers, --dt-force-assignment.ajreynol
2014-08-25New option --purify-triggers. Refactoring of InstMatchGenerator.ajreynol
2014-08-21Avoid doing work in quantifiers engine when no quantifiers are asserted.ajreynol
2014-08-21Fix --inst-max-level for strategies that use arbitrary representative terms.ajreynol
2014-08-18Add support for quantifier-specific instantiation levels. Add option for set...ajreynol
2014-08-01Minor cleanup from previous commit. Better organization for how quantifiers ...ajreynol
2014-07-31New module for generating candidate equality conjectures used in inductive pr...ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-06-19More proof support for CASC : include skolemizationajreynol
2014-05-30Fixes for --inst-max-levelajreynol
2014-05-14Finish --dump-instantiations option. Update scripts.Andrew Reynolds
2014-05-13Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ...ajreynol
2014-05-12Minor updates/fix to --cbqi-recurseAndrew Reynolds
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ...Andrew Reynolds
2014-05-08Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Min...Andrew Reynolds
2014-05-06First draft of ambqi_builder (new implementation of MBQI based on disjoint se...Andrew Reynolds
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-04-28Preparation for models for co-inductive datatypes. Minor cleanup.Andrew Reynolds
2014-04-28Optimizations for datatypes: check for clashes modulo equality. Avoid buildi...ajreynol
2014-04-24Add --inst-max-level=N option for Kshitij. Support define-const command in S...Andrew Reynolds
2014-04-09Handle fmf.card as input from user, add support in SMT2 parser, as requested ...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback