cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2015-03-05	Minor fixes. Extend cegqi-si to real arithmetic.	ajreynol

2015-03-04	More work on arithmetic single invocation synthesis conjectures.	ajreynol

2015-02-26	Robust strategy for single invocation LIA synthesis conjectures. Add ↵	ajreynol
	regressions.
2015-02-25	Switch back to eager loop temporarily.	Tianyi Liang

2015-02-24	minor fix for internal string print	Tianyi Liang

2015-02-22	New trigger options. --inst-no-entail on by default. Misc cleanup.	ajreynol

2015-02-13	Minor cleanup, remove unused files.	ajreynol

2015-02-13	Handle recursive singleton case for codatatypes, add regression. Simplify ↵	ajreynol
	implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
2015-02-11	Better support for solving multiple functions with cegqi-si. Minor cleanup.	ajreynol

2015-02-11	Move si solution reconstruction to own file, make more robust. Other ↵	ajreynol
	refactoring.
2015-02-06	Handle missing cases for single inv solution reconstruction. Minor fixes. ↵	ajreynol
	Refactor.
2015-02-05	Minor clean up	Tianyi Liang

2015-02-05	Improved string performance, thanks to Peter's benchmarks.	Tianyi Liang

2015-02-05	Working version of sygus solution reconstruction from single inv cegqi. ↵	ajreynol
	Heuristics to fit syntax.
2015-02-04	Initial draft of solution reconstruction into syntax for single inv cegqi.	ajreynol

2015-02-04	Work on solution reconstruction for single inv. Fix compiler error found by ↵	ajreynol
	Tim regarding Trace.isOn
2015-02-04	Refactor sygus_util to TermDb. Initial work on solution reconstruction into ↵	ajreynol
	syntax for single inv properties.
2015-02-04	Start work on simplifying single inv solutions. Minor.	ajreynol

2015-02-03	Simple variable elimination for single inv properties. Relax conditions for ↵	ajreynol
	partial inst variables for LTE.
2015-02-03	Solutions for single invocation conjectures.	ajreynol

2015-02-02	Single invocation module for counterexample guided quantifier instantiation ↵	ajreynol
	--cegqi-si. Minor improvements to syntax-guided case, refactoring. Do not apply exhaustive tester inference for sygus datatypes.
2015-02-02	Representative programs must be minimal size, minor fixes, improvements to ↵	ajreynol
	ITE handling in sygus.
2015-02-01	Generalization of sygus lemmas based on arguments and content.	ajreynol

2015-01-31	Bug fix fairness for commutative operators in sygus. Minor.	ajreynol

2015-01-31	Lemmas instead of conflicts in sygus sym break (do not expand explanations). ↵	ajreynol
	Minor improvements to sygus splitting.
2015-01-30	Generalize conflict clauses in sygus sym break, merge caches, refactor. ↵	ajreynol
	Preparation for single invocation properties. Set output lang to SMT2 for sygus.
2015-01-29	Apply sygus search space narrowing for all subprograms of current global state.	ajreynol

2015-01-29	Restrict LtePartialInst instantiations based on E-matching, promote to ↵	ajreynol
	quantifiers module. Refactor QuantifiersEngine registration and check.
2015-01-29	Apply global search space narrowing for multiple synth-fun, enable its ↵	ajreynol
	conflict lemmas.
2015-01-29	Add module for sygus search space narrowing based on global state.	ajreynol

2015-01-28	Minor refactor CEGQI.	ajreynol

2015-01-27	Always miniscope nested quantifiers. Disable miniscoping when cegqi ↵	ajreynol
	enabled. Simplify option names.
2015-01-27	Recognize when synthesis conjectures are in single invocation fragment.	ajreynol

2015-01-26	Output solutions for synthesis conjectures with --dump-synth. Minor ↵	ajreynol
	refactor of previous commit.
2015-01-26	Generalize sygus search space narrowing to arbitrary theory rewriting.	ajreynol

2015-01-24	Variable patterns only look at eligible terms. Minor refactoring of ↵	ajreynol
	quantifiers check for sat.
2015-01-24	Add --lte-restrict-inst-closure option. Push dt.size fairness constraints ↵	ajreynol
	inside splitting lemmas for sygus.
2015-01-23	Refactor sygus arg nf. Minor improvements.	ajreynol

2015-01-23	CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly ↵	ajreynol
	applied selectors.
2015-01-23	Rework inst-closure.	ajreynol

2015-01-22	Narrow sygus search space based on NNF and rewriting constant arguments.	ajreynol

2015-01-22	Add option --lte-partial-inst. Remove inst-closure.	ajreynol

2015-01-22	Do not drop patterns during boolean term rewriting. Narrow sygus search ↵	ajreynol
	space based on commutative operators.
2015-01-21	Avoid redundant constant arguments for SygusNormalForm. Refactor.	ajreynol

2015-01-21	Initial work on sygusNormalForm.	ajreynol

2015-01-20	Mark datatypes as sygus. Add option to normalize sygus terms in search. ↵	ajreynol
	Add sygus regressions.
2015-01-20	Handle miniscoping of conjunctions in synthesis properties. Refactor ↵	ajreynol
	construction of sygus datatypes. Expand define-fun in evaluators.
2015-01-16	Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding ↵	ajreynol
	declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures.
2015-01-16	Minor: Ensure indexed terms are in EE. Add support for bv constants in ↵	ajreynol
	sygus parser.
2015-01-14	sygus input language and benchmark	Morgan Deters