Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-04-07 | Change option names for nl. | ajreynol | |
2017-04-05 | Merge pull request #143 from FabianWolff/master | Clark Barrett | |
Fix several spelling errors | |||
2017-04-05 | Fix bug 698. | ajreynol | |
2017-04-05 | Caching for fun def process, add regression. | ajreynol | |
2017-04-05 | Remove extraneous portion of an nl regression. | ajreynol | |
2017-04-05 | Add non-linear regressions, disable nlAlgSubs, do not do rep checking for ↵ | ajreynol | |
NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver. | |||
2017-04-05 | Fix several spelling errors | Fabian Wolff | |
2017-04-04 | Enable multi-trigger-linear by default, add option. | ajreynol | |
2017-04-04 | Do not solve for 0-ary non-constant symbols (for which isVar returns true), ↵ | ajreynol | |
add regressions. | |||
2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge ↵ | Tim King | |
commit for nlAlgMaster. | |||
2017-03-28 | Refactor the standard effort of relational solver | Paul Meng | |
2017-03-28 | Fix bug 787. | ajreynol | |
2017-03-28 | Fix for bug 733 | Clark Barrett | |
2017-03-24 | Add some regressions. Minor. | ajreynol | |
2017-03-22 | Minor fix for bounded integers. | ajreynol | |
2017-03-20 | fixed cvc4 parser for set complement | Paul Meng | |
2017-03-17 | better support for proof production when encountering bool terms: handle the ↵ | guykatzz | |
new proof constructs generated by the equality engine. proof production for bool-array.smt2 passes | |||
2017-03-16 | More fixes, features to examples. | ajreynol | |
2017-03-16 | Minor fixes, always expand applications of lambdas at preprocess. | ajreynol | |
2017-03-16 | Support for SMT LIB 2.6 syntax declare-datatype and match. | ajreynol | |
2017-03-16 | Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ↵ | ajreynol | |
mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g. | |||
2017-03-15 | Fix regress1 Makefile for rewriterules, fixes bug 783. | ajreynol | |
2017-03-15 | Allow 0 argument recursive functions. Fixes bug 782. | ajreynol | |
2017-03-09 | better proof support for bools and formulas | guykatzz | |
2017-03-07 | More fixes for printing/parsing sets, fix kind name. | ajreynol | |
2017-03-07 | Fix cvc parser for set compliment. | ajreynol | |
2017-03-06 | Support for set compliment and universe set. Simplify approach for sep.nil ↵ | ajreynol | |
nodes. | |||
2017-03-03 | Fix for collectModelInfo related to finite types + preregistration. ↵ | ajreynol | |
Generalize previous fix for sets, minor changes to Datatypes. | |||
2017-03-03 | Another minor fix for sets related to sharing + finite element types. | ajreynol | |
2017-03-02 | Fixes related to sets. | ajreynol | |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ | ajreynol | |
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. | |||
2017-02-07 | Generalize finite bound inference to unifiable variables in set membership ↵ | ajreynol | |
literals. | |||
2017-01-30 | Fix regexp cache issue in strings, add regression. | ajreynol | |
2017-01-18 | Fix non-idempotent rewrite in Array rewriter | Andres Noetzli | |
This commit fixes bug 637 ( http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as proposed in Bugzilla and adds the minified test case to the regression tests. | |||
2017-01-11 | Merge pull request #129 from timothy-king/regression-scrubber | Clark Barrett | |
Adding regression test scrubbing. | |||
2017-01-11 | Fix for when variables are (partially) bound in multiple ways, add ↵ | ajreynol | |
regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed. | |||
2017-01-10 | Adding regression test scrubbing. | Tim King | |
2017-01-05 | Disabling a regression test that assumes CVC4 is configured with proofs on. ↵ | Tim King | |
Modifying the travis rules so there are instances with proofs disabled. | |||
2017-01-04 | Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor ↵ | ajreynol | |
changes. | |||
2017-01-04 | Marking regression test files as non-executable. | Tim King | |
2017-01-04 | Reverting two files encoding with DOS linebreaks back into using unix ↵ | Tim King | |
linebreaks. | |||
2016-12-16 | Fix dependency tracing for fewerPreprocessingHoles | Andres Notzli | |
Previously, dependency tracing in `ite_removal.cpp` was only done with the `unsatCores` option but `fewerPreprocessingHoles` requires dependencies, too. This lead to errors during proof construction when `fewerPreprocessingHoles` was active. This commit fixes the condition and includes a test case that previously failed. Additionally, it fixes a similar issue in the theory engine. NOTE: this commit might not fix all instances of this problem. `smt_engine.cpp` turns certain flags off with `unsatCores`. Compatibility between those flags and `fewerPreprocessingHoles` needs to be checked separately. | |||
2016-12-12 | Fix split-find-unsat-w-emp test | Andres Notzli | |
Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the split-find-unsat-w-emp test, this commit fixes that. | |||
2016-12-08 | Fix (inactive) `MultSlice` rewrite | Andres Notzli | |
The `MultSlice` rewrite was previously accepting multiplications of three and more variables even though it was designed for multiplications of two variables only. Fortunately, the rewrite was not actively used in the bitvector solver. This commit strengthens the condition in `applies()` and adds a unit test that checks that x * y * z and x * y do not get rewritten to the same term. | |||
2016-12-08 | Enable remaining cardinality benchmarks | ajreynol | |
2016-12-07 | Add missing regression | ajreynol | |
2016-12-07 | Add sets regression, fixes bug 754. Minor fix to regexp in strings. | ajreynol | |
2016-12-07 | Added cardinality to cvc language, fixes bug 753. Throw logic exception when ↵ | ajreynol | |
using cardinality on sets with finite element type. | |||
2016-12-07 | Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764. | ajreynol | |
2016-12-07 | Refactoring, generalization of bounded inference module. Simplification of ↵ | ajreynol | |
rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions. |