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

Age	Commit message (Collapse)	Author
2018-07-14	Merge branch 'master' into fixExportTofixExportTo	Andrew Reynolds

2018-07-14	sygusComp2018: update semantics for declare-fun in sygus. (#2102)	Andrew Reynolds

2018-07-14	Fix and improve grammar normalization for any constant. (#2101)	Andrew Reynolds

2018-07-13	Properly clean up assertion stack in CnfProof (#2147)	Andres Noetzli
	Fixes issue #2137. CnfProof has a stack of assertions that are being converted to clauses. Previously, it could happen that while an assertion was being added, TheoryProxy::explainPropagation() would be called from Solver::reason() and push an assertion to the stack that was then not removed. This lead to a clause id of the assertion being associated with the explanation instead, which in turn could lead to a wrong unsat core. This commit identifies two cases where TheoryProxy::explainPropagation() is called without cleaning up the assertion stack afterwards. It also adds an assertion that the assertion stack must be empty when we are getting the unsat core.
2018-07-13	exportTo only if needed for --sygus-rr-synth-check	Andres Noetzli
	With this commit, we only use an SmtEngine with a separate ExprManager for --sygus-rr-synth-check if necessary (currently, this is only the case when --sygus-rr-synth-check-timeout is active). The reason for this is that we do not support exportTo for all kinds. Additionally, this commit adds support for exporting floating-point types and adds a check that throws an exception if an unsupported type is being exported (previously, it just crashed). Finally, it fixes a minor issue with -d export, where an expression was printed while the wrong ExprManager was active, leading to an assertion failure when getting the types of expressions (which is required for operators like equality where the sort of the children is not fixed).
2018-07-13	sygusComp2018: optimization for collect model info (#2105)	Andrew Reynolds

2018-07-13	New C++ API: Minor reorder. (#2163)	Aina Niemetz

2018-07-13	New C++ API: Implementation of datatype classes. (#2142)	Aina Niemetz

2018-07-13	New C++ API: Implementation of Solver class: Consts handling. (#2145)	Aina Niemetz

2018-07-10	Move rewrite to pass (#2128)	Caleb Donovick

2018-07-08	Add more sophisticated floating-point sampler (#2155)	Andres Noetzli
	This commit adds a floating-point sampler inspired by PyMPF [0]. It also creates a new Sampler class that can be used for creating random values of different sorts (currently BV and FP values). [0] https://github.com/florianschanda/PyMPF
2018-07-06	sygusComp2018: improve extended rewriter for Bool (#2107)	Andrew Reynolds

2018-07-06	Split ext theory to own file and document (#1809)	Andrew Reynolds

2018-07-06	Feature/fp rewrite improvement (#2154)	Martin

2018-07-06	New C++ API: Implementation of Solver class: Term handling. (#2144)	Aina Niemetz

2018-07-06	New C++ API: Implementation of Solver class: Sort handling. (#2143)	Aina Niemetz

2018-07-06	Add option for timeout for rewrite candidate check (#2156)	Andres Noetzli

2018-07-06	sygusComp2018: simplify beta reduction in uf rewriter. (#2106)	Andrew Reynolds
	This is PR 8/18 from the sygus comp 2018 branch (https://github.com/ajreynol/CVC4/tree/sygusComp2018-2). I am not sure how it is possible in any circumstance that the complication in the comment I am deleting would ever happen, without doing something very strange. I think it is referring to some sort of inter-dependence between macro expansion + beta-reductions. This should not concern the rewriter. Here is the commit that introduced it: bdaa304.
2018-07-05	Make string length lemmas more robust to rewriting (#2150)	Andrew Reynolds

2018-07-04	Minor changes to sygus-rr utilities to support floating point rewrites (#2148)	Andrew Reynolds

2018-07-05	sygusComp2018: Improve string rewriter (#2141)	Andres Noetzli

2018-07-04	More cleanup in strings (#2138)	Andrew Reynolds

2018-07-04	New C++ API: Implementation of datatype declaration classes. (#2136)	Aina Niemetz

2018-07-04	Reorganize candidate rewrite rule filtering (#2116)	Andrew Reynolds

2018-07-04	Remove unused CDVector (#2139)	Andres Noetzli

2018-07-04	New C++ API: Implementation of OpTerm. (#2132)	Aina Niemetz

2018-07-03	Fix fmf-fun for non-equality function definitions (#2134)	Andrew Reynolds
	Fixes #2133. In that issue, a quantifiers rewrite triggered a model-unsoundness in fmf-fun. The rewrite made a function definition have an ITE at top-level instead of equality. The corrected code was model-unsound, since it assumed that quantified formulas that are not EQUAL can be ignored.
2018-07-03	New C++ API: Implementation of Term. (#2131)	Aina Niemetz

2018-07-03	New C++ API: Implementation of Kind maps. (#2130)	Aina Niemetz

2018-07-03	Fix datatypes example: nil constructor was missing. (#2135)	Aina Niemetz

2018-07-02	sygusComp2018: update sygus-related options setting in smt engine (#2108)	Andrew Reynolds

2018-07-02	Remove miscellaneous dead and unused code from quantifiers (#2121)	Andrew Reynolds

2018-07-02	Add regression test for issue #1986 (#2114)	Andres Noetzli
	The issue is not triggered anymore after PR #2059 but the test case is good to have for changes in MiniSat code.
2018-07-02	Refactor ApplySubsts preprocessing pass. (#2120)	Aina Niemetz

2018-07-02	New C++ API: Implementation of Sort. (#2122)	Aina Niemetz

2018-07-02	Remove some dead code from theory strings (#2125)	Andrew Reynolds

2018-07-02	Add missing include (#2127)	Caleb Donovick

2018-07-02	Modify cegqi heuristic for finite datatypes (#2126)	Andrew Reynolds

2018-07-02	Improve error message. (#2124)	Andrew Reynolds

2018-06-29	Use evaluator in sygus sampler. (#2117)	Andrew Reynolds
	* Use evaluator for sygus sampler. * Format
2018-06-28	New C++ API: Implementation of Result. (#2112)	Aina Niemetz

2018-06-28	Remove comment about model value hack (#2118)	Andrew Reynolds
	This fixes #821. For some background, some special cases were added to equality engine and theory engine a few years ago to handle constants properly. As a result of these changes, a comment in the code was added about a HACK for getModelValue, but the code is completely reasonable looking to me (it says that the model value of a constant is itself). This PR removes that comment. From what I can tell issue #821 can be closed.
2018-06-28	sygusComp2018: optimization for invariance test (#2104)	Andrew Reynolds

2018-06-28	Fix stale reference in MiniSat when generating UC (#2113)	Andres Noetzli
	In MiniSat's analyze(), we were taking a reference of a clause that could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can lead to allocation of clauses which in turn can lead to clauses being reallocated, making the reference stale. The commit encloses the reference in a code block that makes the lifetime of the reference more obvious and removes uses of the potentially stale reference.
2018-06-28	Do not rename uninterpreted constants (#2098)	Andrew Reynolds

2018-06-28	Split and document ceg theory instantiators (#2094)	Andrew Reynolds

2018-06-27	Header for new C++ API. (#1697)	Aina Niemetz

2018-06-27	Synthesize candidate-rewrites from standard inputs (#1918)	Andrew Reynolds

2018-06-26	sygusComp2018: add scripts. (#2103)	Andrew Reynolds

2018-06-26	sygusComp2018: Add evaluator (#2090)	Andres Noetzli
	This commit adds the Evaluator class that can be used to quickly evaluate terms under a given substitution without going through the rewriter. This has been shown to lead to significant performance improvements on SyGuS PBE problems with a large number of inputs because candidate solutions are evaluated on those inputs. With this commit, the evaluator only gets called from the SyGuS solver but there are potentially other places in the code that could profit from it.