summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
AgeCommit message (Expand)Author
2015-08-12Improvements to --macros-quant. Enable --clause-split by default. Bug fix for...ajreynol
2015-08-01Support for default grammar for datatypes in sygus. Support vts for infinity.ajreynol
2015-07-31Sygus support for inductive datatypes.ajreynol
2015-07-30Implement virtual term substitution for non-nested quantifiers. Fix soundnes...ajreynol
2015-07-25Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/...ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-07-12Add option --full-saturate-quant-rd. Fix option --register-quant-body-terms.ajreynol
2015-07-02On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force n...ajreynol
2015-07-01Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-qu...ajreynol
2015-06-29Module to infer alpha equivalence of quantified formulas. Minor clean up of ...ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de...ajreynol
2015-06-16Avoid completion for large finite types. Fix bug for --fmf-fun.ajreynol
2015-06-15Make array basis term a skolem (avoids crashing in fmf).smtcomp2015-stableajreynol
2015-06-12Make sygus an output language. Parse declare-fun in sygus. Minor improvemen...ajreynol
2015-06-12Accelerate sygus solution reconstruction for constants and id functions. Min...ajreynol
2015-06-11Update experimental scripts. Support top-level non-terminals in sygus gramma...ajreynol
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
2015-06-10Parse support for sygus LetGTerm.ajreynol
2015-05-15Avoid ensureLiteral on unpreprocessed formulas in cbqi.ajreynol
2015-05-11Support for arbitrary constants/variables in Sygus grammars.ajreynol
2015-05-10Minor improvements to infrastructure. Minor changes to default options. Add t...ajreynol
2015-04-16Fix option --quant-fun-wd. Add mk_starexec script to contrib.ajreynol
2015-04-08Make fun-def quantifiers carry the function app they define, make fun-def uti...ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback