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

Age	Commit message (Collapse)	Author
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.
2014-03-12	Work on array pf signature, add working example. Add quantifiers proof ↵	Andrew Reynolds
	signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
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-03-04	Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵	Morgan Deters
	(resolves bug #548).
2014-02-25	Add options --full-saturate-quant and --mbqi=trust. Other minor changes.	Andrew Reynolds

2014-01-28	More optimizations of quantifier instantiation data structures.	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-18	Performance optimization for E-matching, working on using QCF module for ↵	Andrew Reynolds
	propagations.
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.
2014-01-03	Removing and consolidating options for uf-ss and quantifiers. Bug fix for ↵	Andrew Reynolds
	inst gen-style MBQI.
2014-01-03	Added support for proof production in Equality Engine. Cleaned up existing ↵	Andrew Reynolds
	proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.