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

Age	Commit message (Collapse)	Author
2014-04-29	Mostly resolves bug #561 memory leaks, and more.	Morgan Deters

2014-04-28	Merge pull request #25 from kbansal/sets	Kshitij Bansal
	Sets
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-28	Merge remote-tracking branch 'upstream/master' into sets	Kshitij Bansal

2014-04-24	Add --inst-max-level=N option for Kshitij. Support define-const command in ↵	Andrew Reynolds
	Smt2.
2014-04-17	Allow fmf-bound-int to be set with set-option and via API.	Morgan Deters

2014-04-17	simplify mkSkolem naming system: don't use $$	Kshitij Bansal
	Short summary: By default NODEID is appeneded, just continue doing what you were, just don't add the _$$ at the end. Long summary: Before this commit there were four (yes!) ways to specify the names for new skolems, which result in names as given below 1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 2) mkSkolem("name", ..., SKOLEM_EXACT_NAME) -> "name" 3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me" After this commit, only 1) and 2) stay. 90% usage is of 1) or 3), which results in exact same behavior (and looking at the source code it doesn't look like everyone realized that the _$$ is just redundant). Almost no one used 4), which is the only reason to even have $$. Post this commit if you really want a number in the middle, manually construct the name and use the SKOLEM_EXACT_NAME flag.
2014-04-14	Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ↵	Andrew Reynolds
	Improve datatypes rewrite, make option for previous dt semantics.
2014-04-10	Expand definitions in theory datatypes, now has the expected semantics for ↵	Andrew Reynolds
	incorrectly applied selector terms.
2014-04-10	Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵	Andrew Reynolds
	Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
2014-04-09	Revert E-matching datatypes fix.	Andrew Reynolds

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-20	Minor fix for CBQI, ignore inst constant nodes.	Andrew Reynolds

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-12	Minor fixes post-merge of RR.	Andrew Reynolds

2014-03-11	Fix for rewriterules build breakage.	Morgan Deters

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-07	Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵	Morgan Deters
	bodies; fix bug 551, improper ITE removal under quantifiers.
2014-03-04	Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵	Morgan Deters
	(resolves bug #548).
2014-02-27	Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the ↵	Andrew Reynolds
	default QCF setting. Bug fix to prevent non-ground terms from entering relevant domains.
2014-02-25	Add options --full-saturate-quant and --mbqi=trust. Other minor changes.	Andrew Reynolds

2014-02-21	fix a -Wunused	Kshitij Bansal

2014-02-20	Fix ite and iff handling in QCF. Add option for heuristic instantiation in ↵	Andrew Reynolds
	QCF (not working yet). Improve automatic option setting for quantifiers.
2014-02-14	Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add ↵	Andrew Reynolds
	support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
2014-02-09	More complete guess instantiation strategy, cvc4 now typically times out ↵	Andrew Reynolds
	instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
2014-02-05	Bug fix for theory strings related to old cycle detection code (was leading ↵	Andrew Reynolds
	to bogus model). Minor cleanup of QCF.
2014-02-04	Add variable ordering for QCF to accelerate matching procedure. Preparing ↵	Andrew Reynolds
	for QCF_MC mode.
2014-02-03	Handle nested (universal) quantifiers in QCF algorithm. Make relevant ↵	Andrew Reynolds
	domain instantiation breadth-first.
2014-01-30	Refactor QCF slightly. Bug fix for relevant domain (non-ground terms were ↵	Andrew Reynolds
	added). Bug fix for QCF (was missing instantiations due to not using getRepresentative).
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-24	Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry ↵	Andrew Reynolds
	approach. Minor change to quantifier macros. Add option --quant-cf-mode.
2014-01-22	Smarter options, but still have a bug	Tianyi Liang

2014-01-22	Delay QuantifiersEngine and UF strong solver initialization until after ↵	Morgan Deters
	final options/logic are set.
2014-01-18	Fixed non-termination issue in bounded integers.	Andrew Reynolds

2014-01-18	Performance optimization for E-matching, working on using QCF module for ↵	Andrew Reynolds
	propagations.
2014-01-17	More optimizations for quantifiers conflict find. Add trust user patterns mode.	Andrew Reynolds

2014-01-15	Optimizations for quantifiers conflict find: better caching, process ↵	Andrew Reynolds
	matching constraints eagerly.
2014-01-10	Add stats to quantifiers conflict find. Added option for qcf. Working on ↵	Andrew Reynolds
	handling non-APPLY_UF terms.
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.
2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

2013-11-27	General pre-release cleanup commit	Morgan Deters
	* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing
2013-11-26	Bug fix for E-matching select terms, minor fix for bounded integers, bug fix ↵	Andrew Reynolds
	to improve performance of quantifiers rewriter
2013-11-10	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

2013-11-06	Bug fixes for bounded integer quantification. Current best strategy is to ↵	Andrew Reynolds
	turn off MBQI. Disable relevant triggers by default.
2013-10-07	Multiple fixes for datatypes theory solver: add support for parametric ↵	Andrew Reynolds
	datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.