summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
AgeCommit message (Expand)Author
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add regress...ajreynol
2015-02-11Better support for solving multiple functions with cegqi-si. Minor cleanup.ajreynol
2015-02-11Move si solution reconstruction to own file, make more robust. Other refactor...ajreynol
2015-02-06Handle missing cases for single inv solution reconstruction. Minor fixes. Re...ajreynol
2015-02-05Working version of sygus solution reconstruction from single inv cegqi. Heur...ajreynol
2015-02-04Work on solution reconstruction for single inv. Fix compiler error found by ...ajreynol
2015-02-04Refactor sygus_util to TermDb. Initial work on solution reconstruction into ...ajreynol
2015-02-04Start work on simplifying single inv solutions. Minor.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
2015-01-16Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding de...ajreynol
2015-01-16Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus...ajreynol
2014-11-25Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos...ajreynol
2014-11-18Compute model basis only for fmf. Add another co-datatype regression.ajreynol
2014-11-18Add local theory extensions instantiation strategy (incomplete). Refactor ho...ajreynol
2014-11-16Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e...ajreynol
2014-11-14Be lazier to consider EQC in UF+cardinality solver. Minor cleanup.ajreynol
2014-11-13Remove two obsolete versions of MBQI.ajreynol
2014-11-13More preparation for filtering relevant terms in TermDb.ajreynol
2014-11-11Work on synchronizing decision=justification and E-matching.ajreynol
2014-11-10Do not eliminate variables only occurring in patterns. Minor improvements to...ajreynol
2014-11-01Fix some mistakes in datatypes theory combination, disable two regressions. ...ajreynol
2014-10-31Do not allow duplication of function definitions. Set incomplete flag in mod...ajreynol
2014-10-28Preprocessing step for finding finite runs of well-defined function definitio...ajreynol
2014-10-28Initial infrastructure for function definition quantifiers, internal parsing ...ajreynol
2014-10-10Initial draft of CEGQI.ajreynol
2014-10-10Add owner map to better manage QuantifiersModules. Initial infrastructure fo...ajreynol
2014-10-07Refactor quantifiers attributes.ajreynol
2014-09-16Refactoring of conjecture generator. Determine subgoals are non-canonical ba...ajreynol
2014-08-29Set instantiation level on skolemized bodies of quantifiers. Rename inst-lev...ajreynol
2014-08-20Add option for inductive strengthening based on well-founded induction for in...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-22Renaming of SMT2 operator names, kinds for set theoryKshitij Bansal
2014-06-03Support E-matching/QCF for Set operators.ajreynol
2014-05-30Improve --dt-stc-ind for multi-variable datatype properties.ajreynol
2014-05-23Fix bug in E-matching Real/Int terms.Andrew Reynolds
2014-05-08Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Min...Andrew Reynolds
2014-05-02Fix assertion from previous commit.ajreynol
2014-05-02Add option --dt-stc-ind for strengthening skolemization. Refactor skolemizat...Andrew Reynolds
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-17simplify mkSkolem naming system: don't use $$Kshitij Bansal
2014-04-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ...Andrew Reynolds
2014-04-09Revert E-matching datatypes fix.Andrew Reynolds
2014-04-09Handle fmf.card as input from user, add support in SMT2 parser, as requested ...Andrew Reynolds
2014-03-12Work on array pf signature, add working example. Add quantifiers proof signa...Andrew Reynolds
2014-03-11Fix for rewriterules build breakage.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback