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

Age	Commit message (Collapse)	Author
2015-10-31	Improvements to handling of mixed Int/Real quantifiers.	ajreynol

2015-10-26	Promote InstStrategyCbqi to quantifier module. Cleanup unused code.	ajreynol

2015-10-26	Extend counterexample-guided instantiation to extended theory of Int/Real, ↵	ajreynol
	mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
2015-09-28	Improve quantifiers engine wrt incremental presolve. Add regressions.	ajreynol

2015-09-26	Better organization of quantifiers modules, promote full saturation to ↵	ajreynol
	module. Add heuristics for cbqi LIA instantiation with coefficients.
2015-09-25	Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ↵	ajreynol
	of term database, other refactoring. Bug fixes for cbqi+datatypes.
2015-09-18	Fix bug in quantifiers engine where model construction could be skipped.	ajreynol

2015-09-15	Fix bug related to quantifiers + incremental, thanks John Backes for the bug ↵	ajreynol
	report. Other minor cleanup.
2015-08-26	Minor improvements to cbqi, fix bug in solving with vts symbols, round up ↵	ajreynol
	for integer lower bounds. Add presolve infrastructure to quantifiers engine, modify --cbqi-prereg-inst.
2015-08-12	Improvements to --macros-quant. Enable --clause-split by default. Bug fix ↵	ajreynol
	for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
2015-07-30	Implement virtual term substitution for non-nested quantifiers. Fix ↵	ajreynol
	soundness bug in strings related to explaining length terms.
2015-07-20	Squashed merge of SygusComp 2015 branch.	ajreynol

2015-06-29	Module to infer alpha equivalence of quantified formulas. Minor clean up of ↵	ajreynol
	options.
2015-06-27	Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by ↵	ajreynol
	default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
2015-06-22	Add --user-pat=interleave. Remove unused lte inst strategy.	ajreynol

2015-05-15	Avoid ensureLiteral on unpreprocessed formulas in cbqi.	ajreynol

2015-05-13	Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ↵	ajreynol
	for sygus.
2015-05-10	Minor improvements to infrastructure. Minor changes to default options. Add ↵	ajreynol
	tff script. Minor additions to sygus.
2015-03-11	Minor fixes and improvements to cegqi-si for linear arithmetic.	ajreynol

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-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-13	Remove two obsolete versions of MBQI.	ajreynol

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	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-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-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-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-03-11	Initial refactor of rewrite rules, make theory_rewriterules empty theory. ↵	Andrew Reynolds
	Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter. Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up. QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master. Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern. Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE. Merging rewrite rules into master, check-model current fails on 3 FMF regressions. Fix check-model issue, a line of code was omitted during merge.
2014-02-25	Add options --full-saturate-quant and --mbqi=trust. Other minor changes.	Andrew Reynolds

2014-01-27	More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.	Andrew Reynolds

2014-01-26	More optimization of QCF. Fixed InstMatchTrie for caching instantiations. ↵	Andrew Reynolds
	Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
2014-01-10	Add new method --quant-cf for finding conflicts eagerly for quantified ↵	Andrew Reynolds
	formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.