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

Age	Commit message (Collapse)	Author
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-10	Support for printing solutions involving LetGTerm sygus. Bug fix define-fun ↵	ajreynol
	within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
2015-06-09	Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization ↵	ajreynol
	for non-UF logics. Update SMT COMP scripts accordingly.
2015-06-01	When proof enabled, disable uf sym break. Add regression.	ajreynol

2015-05-29	changed resource step options to unsigned	lianah

2015-05-28	added options for controlling resource step-count for various solving stages	Liana Hadarean

2015-05-11	Allow sygus with no syntactic restrictions for LIA. Add regressions.	ajreynol

2015-05-10	Minor improvements to infrastructure. Minor changes to default options. Add ↵	ajreynol
	tff script. Minor additions to sygus.
2015-04-23	Merge branch 'master' into google	Clark Barrett

2015-04-23	Added option for --check-unsat-cores and various core bug fixes (merge of ↵	Liana Hadarean
	Morgan's proof branch).
2015-04-21	Changes needed to compile at Google, plus some bug fixes from Google.	Clark Barrett

2015-04-15	Fix for unconstrained bug.	Clark Barrett

2015-04-09	Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, ↵	ajreynol
	and strings preprocessing. Minor fix for conjecture generation for finite types.
2015-04-01	Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with ↵	ajreynol
	fun-def. Add skolemization options.
2015-03-23	Decouple counter-example guided quantifier instantiation from Sygus.	ajreynol

2015-03-16	Fixed proof unitialized memory and minor memory leaks.	Liana Hadarean

2015-03-10	CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵	ajreynol
	signature. Add regressions.
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-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-01-27	Always miniscope nested quantifiers. Disable miniscoping when cegqi ↵	ajreynol
	enabled. Simplify option names.
2015-01-26	Output solutions for synthesis conjectures with --dump-synth. Minor ↵	ajreynol
	refactor of previous commit.
2015-01-22	Narrow sygus search space based on NNF and rewriting constant arguments.	ajreynol

2015-01-22	Do not drop patterns during boolean term rewriting. Narrow sygus search ↵	ajreynol
	space based on commutative operators.
2015-01-13	Fix a memory issue in ResourceManager on 32-bit (resolves bug #606).	Morgan Deters

2014-12-28	Disable prenex by default when using fmf bound int, minor improvement to ↵	ajreynol
	datatypes rewriter
2014-12-16	Fix oversight in dumping assertions in preprocessing.	Morgan Deters

2014-12-04	Fix segfault in lambdas when constructed via API.	Morgan Deters

2014-12-03	Floating point infrastructure.	Martin Brain
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-11-22	added number of resource units used as a stat	lianah

2014-11-21	Change default option to --inst-when=full-last-call (interleave ↵	ajreynol
	instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.
2014-11-18	Set Constant's normal form and other short fixes	Kshitij Bansal
	Other short fixes: * use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT * theoryof-mode fix in smt_engine.cpp * hack in TheoryModel::getModelValue [TODO: notify Clark/Andy] * Lemma generation when it rewrites to true/false fix * TermInfoManager::addTerm(..) fix * Move SUBSET rewrite to preRewrite * On preRegister, queue up propagation to be done upfront ** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code. * TheorySetsProperties::getCardinality(..) fix Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing!
2014-11-18	Add local theory extensions instantiation strategy (incomplete). Refactor ↵	ajreynol
	how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
2014-11-17	Resource-limiting work.	Liana Hadarean
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-11-13	Remove two obsolete versions of MBQI.	ajreynol

2014-11-09	Merge branch '1.4.x'	Morgan Deters

2014-11-09	Fix a deterministic assignment-ordering for get-assignment (fixes a ↵	Morgan Deters
	regression failure on Mac).
2014-11-07	Merge branch '1.4.x'	Morgan Deters
	Conflicts: src/smt/model_postprocessor.cpp test/regress/regress0/Makefile.am
2014-11-07	Fix missing case in Boolean terms rewriting. (Resolves bug #596.)	Morgan Deters

2014-11-07	Merge branch '1.4.x'	Morgan Deters
	Conflicts: src/smt/model_postprocessor.cpp
2014-11-07	Corrected fix for missing case in model postprocessor (resolves bug #595).	Morgan Deters

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	Revert "Fix missing case in model postprocessor (resolves bug #595)."	Morgan Deters
	This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.
2014-11-07	Revert "Fix missing case in model postprocessor (resolves bug #595)."	Morgan Deters
	This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. Conflicts: test/regress/regress0/Makefile.am
2014-11-07	Merge branch '1.4.x'	Morgan Deters
	Conflicts: test/regress/regress0/Makefile.am
2014-11-07	Fix missing case in model postprocessor (resolves bug #595).	Morgan Deters

2014-10-28	Preprocessing step for finding finite runs of well-defined function ↵	ajreynol
	definitions using FMF.
2014-10-23	Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.	Morgan Deters
	* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.)
2014-10-16	Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ↵	ajreynol
	changes to options.
2014-10-14	Context-dependent expr attributes are now attached to a specific SmtEngine, ↵	Morgan Deters
	and the SAT context is owned by the SmtEngine.