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

Age	Commit message (Collapse)	Author
2015-02-04	Refactor sygus_util to TermDb. Initial work on solution reconstruction into ↵	ajreynol
	syntax for single inv properties.
2015-01-29	Restrict LtePartialInst instantiations based on E-matching, promote to ↵	ajreynol
	quantifiers module. Refactor QuantifiersEngine registration and check.
2015-01-26	Output solutions for synthesis conjectures with --dump-synth. Minor ↵	ajreynol
	refactor of previous commit.
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	Rework inst-closure.	ajreynol

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

2014-11-28	Synchronize conjecture generation with E-matching. Minor fix to ↵	ajreynol
	--full-saturate-quant.
2014-11-25	Fix bug in --term-db-mode=relevant with variable triggers. Support ↵	ajreynol
	inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers.
2014-11-20	Disable constants sharing in eq engine, disable hack in theory engine. ↵	ajreynol
	Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
2014-11-18	Compute model basis only for fmf. Add another co-datatype regression.	ajreynol

2014-11-13	Remove two obsolete versions of MBQI.	ajreynol

2014-11-07	Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor ↵	ajreynol
	improvement to performance of E-matching.
2014-11-07	Properly distinguish which EQC to assign values in datatypes, use ↵	ajreynol
	assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.
2014-10-13	CEGQI uses model. Enforce fairness in CEGQI natively.	ajreynol

2014-10-13	Model building into quantifiers engine. Simplify axiom-inst mode.	ajreynol

2014-10-13	Refactor 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-10	Initial draft of CEGQI.	ajreynol

2014-10-10	Add owner map to better manage QuantifiersModules. Initial infrastructure ↵	ajreynol
	for cegqi.
2014-10-08	Cache for getInstance, thanks to Johannes Kanig for the report. Do not ↵	ajreynol
	mkRep for multi triggers.
2014-10-07	Refactor quantifiers attributes.	ajreynol

2014-10-06	Fix a resource limiting issue where interruption didn't occur promptly. ↵	Morgan Deters
	Thanks Johannes Kanig for the report.
2014-09-26	Finer-grained resource-limiting in quantifiers.	Morgan Deters

2014-09-24	Refactor option for uf+cardinality constraints solver.	ajreynol

2014-09-23	Do not throw error when codatatype is not well-founded. Add option for ↵	ajreynol
	disabling codatatype reasoning. Minor cleanup.
2014-09-18	Resource spending support in theories (and especially in quantifiers).	Morgan Deters

2014-09-16	Bug fix variable triggers with --inst-max-level : use term in EQC with ↵	ajreynol
	minimal instantiation level.
2014-09-09	Accept user-provided triggers with variable terms. Flush lemmas before ↵	ajreynol
	quantifiers check. Minor fix for conjecture generation.
2014-08-29	Set instantiation level on skolemized bodies of quantifiers. Rename ↵	ajreynol
	inst-level attribute to quant-inst-max-level
2014-08-26	Bug fixes for --purify-triggers, --dt-force-assignment.	ajreynol

2014-08-25	New option --purify-triggers. Refactoring of InstMatchGenerator.	ajreynol

2014-08-21	Avoid doing work in quantifiers engine when no quantifiers are asserted.	ajreynol

2014-08-21	Fix --inst-max-level for strategies that use arbitrary representative terms.	ajreynol

2014-08-18	Add support for quantifier-specific instantiation levels. Add option for ↵	ajreynol
	setting inst-level 0 only for input terms.
2014-08-01	Minor cleanup from previous commit. Better organization for how quantifiers ↵	ajreynol
	modules check (introduce QuantifiersEngine::QEffort).
2014-07-31	New module for generating candidate equality conjectures used in inductive ↵	ajreynol
	proofs. Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness. Refactoring of term database. QcfEngine now uses central data structure for term indexing. Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).
2014-07-01	Update copyrights.	Morgan Deters

2014-06-19	More proof support for CASC : include skolemization	ajreynol

2014-05-30	Fixes for --inst-max-level	ajreynol

2014-05-14	Finish --dump-instantiations option. Update scripts.	Andrew Reynolds

2014-05-13	Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ↵	ajreynol
	Add regressions.
2014-05-12	Minor updates/fix to --cbqi-recurse	Andrew Reynolds

2014-05-11	More preparation for CASC proofs. Minor fix for sort inference (rewrite new ↵	Andrew Reynolds
	assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
2014-05-08	Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. ↵	Andrew Reynolds
	Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
2014-05-06	First draft of ambqi_builder (new implementation of MBQI based on disjoint ↵	Andrew Reynolds
	sets).
2014-04-29	Mostly resolves bug #561 memory leaks, and more.	Morgan Deters

2014-04-28	Preparation for models for co-inductive datatypes. Minor cleanup.	Andrew Reynolds

2014-04-28	Optimizations for datatypes: check for clashes modulo equality. Avoid ↵	ajreynol
	building model at fullModel=false when possible. Minor cleanup.
2014-04-24	Add --inst-max-level=N option for Kshitij. Support define-const command in ↵	Andrew Reynolds
	Smt2.
2014-04-09	Handle fmf.card as input from user, add support in SMT2 parser, as requested ↵	Andrew Reynolds
	by Martin Brain. Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.