Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | Allow 0 argument recursive functions. Fixes bug 782. | ajreynol | |
2017-03-14 | fix uninitialized variable | Andres Notzli | |
2017-03-10 | Minor fix for cbqi-all. | ajreynol | |
2017-03-09 | bug fix | guykatzz | |
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 | Do not eagerly construct explanations in relation solver. | ajreynol | |
2017-03-06 | Support for set compliment and universe set. Simplify approach for sep.nil ↵ | ajreynol | |
nodes. | |||
2017-03-06 | Adding support for bool-to-bv | Clark Barrett | |
Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz <katz911@gmail.com> Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass. | |||
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 | Minor cleanup and reorganization related to last commit. | 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-16 | Minor fixes for relations, quantifiers dsplit. | ajreynol | |
2017-02-16 | Fixes for sets+rels check. Minor. | ajreynol | |
2017-02-15 | Minimization modes for fmf bound. | ajreynol | |
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-18 | Minor fix in relations. | ajreynol | |
2017-01-13 | Fix call to SExpr constructor for greater portability. | Clark Barrett | |
2017-01-13 | Merge pull request #130 from chadbrewbaker/master | Clark Barrett | |
Fixing memory leak | |||
2017-01-13 | Do not rewrite explanations in strings. | ajreynol | |
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 | revert | Chad Brewbaker | |
2017-01-10 | Quashing memory leak | Chad Brewbaker | |
2017-01-10 | Adding regression test scrubbing. | Tim King | |
2017-01-08 | With reference to Bug 679, this commit integrates part of the patch ↵ | Cristian Mattarei | |
proposed, and it fixes the correct float parsing of an std::istringstream. The compilation issue in Bug 679 does not apply anymore with gcc6.3.1 | |||
2017-01-06 | quashing debug memory leak | Chad Brewbaker | |
2017-01-06 | Minor fix for sets. | ajreynol | |
2017-01-04 | Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor ↵ | ajreynol | |
changes. | |||
2017-01-04 | Merge pull request #120 from 4tXJ7f/fix_f_pp_holes | guykatzz | |
Fix dependency tracing for fewerPreprocessingHoles | |||
2016-12-29 | Changing a set of TNodes to a set of Nodes in the BV inequality solver. The ↵ | Tim King | |
ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail. | |||
2016-12-29 | Eliminating a signed vs. unsigned comparison. | Tim King | |
2016-12-29 | Changing getTearDownIncremental() to return the type of ↵ | Tim King | |
options::tearDownIncremental. | |||
2016-12-29 | Adding a destructor to InstantiationNotify. | Tim King | |
2016-12-29 | Adding a destructor to RepBoundExt. | Tim King | |
2016-12-29 | Reordering sep and sets in Makefile.theories. | Tim King | |
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-14 | Switch from SMT-LIB v2.0 to v2.5 for smt2 files | Andres Notzli | |
As mentioned in bug 741, CVC4 was parsing `.smt2` files using the SMT-LIB v2.0 standard by default. This commit switches to v2.5. | |||
2016-12-14 | Made tear-down-incremental more like it used to be: when tear-down value | Clark Barrett | |
is 1, it does not automatically enable incremental mode. | |||
2016-12-11 | Merge branch 'master' into fix_order | Clark Barrett | |
2016-12-11 | Merge pull request #116 from 4tXJ7f/fix_mult | Clark Barrett | |
Fix (inactive) `MultSlice` rewrite |