summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-03-16More fixes, features to examples.ajreynol
2017-03-16Minor fixes, always expand applications of lambdas at preprocess.ajreynol
2017-03-16Support for SMT LIB 2.6 syntax declare-datatype and match.ajreynol
2017-03-16Parsing 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-15Allow 0 argument recursive functions. Fixes bug 782.ajreynol
2017-03-14fix uninitialized variableAndres Notzli
2017-03-10Minor fix for cbqi-all.ajreynol
2017-03-09bug fixguykatzz
2017-03-09better proof support for bools and formulasguykatzz
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-07Fix cvc parser for set compliment.ajreynol
2017-03-06Do not eagerly construct explanations in relation solver.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil ↵ajreynol
nodes.
2017-03-06Adding support for bool-to-bvClark 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-03Fix for collectModelInfo related to finite types + preregistration. ↵ajreynol
Generalize previous fix for sets, minor changes to Datatypes.
2017-03-03Another minor fix for sets related to sharing + finite element types.ajreynol
2017-03-02Fixes related to sets.ajreynol
2017-03-02Minor cleanup and reorganization related to last commit.ajreynol
2017-03-02Eliminate 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-16Minor fixes for relations, quantifiers dsplit.ajreynol
2017-02-16Fixes for sets+rels check. Minor.ajreynol
2017-02-15Minimization modes for fmf bound.ajreynol
2017-02-07Generalize finite bound inference to unifiable variables in set membership ↵ajreynol
literals.
2017-01-30Fix regexp cache issue in strings, add regression.ajreynol
2017-01-18Fix non-idempotent rewrite in Array rewriterAndres 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-18Minor fix in relations.ajreynol
2017-01-13Fix call to SExpr constructor for greater portability.Clark Barrett
2017-01-13Merge pull request #130 from chadbrewbaker/masterClark Barrett
Fixing memory leak
2017-01-13Do not rewrite explanations in strings.ajreynol
2017-01-11Merge pull request #129 from timothy-king/regression-scrubberClark Barrett
Adding regression test scrubbing.
2017-01-11Fix 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-10revertChad Brewbaker
2017-01-10Quashing memory leakChad Brewbaker
2017-01-10Adding regression test scrubbing.Tim King
2017-01-08With 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-06quashing debug memory leakChad Brewbaker
2017-01-06Minor fix for sets.ajreynol
2017-01-04Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor ↵ajreynol
changes.
2017-01-04Merge pull request #120 from 4tXJ7f/fix_f_pp_holesguykatzz
Fix dependency tracing for fewerPreprocessingHoles
2016-12-29Changing 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-29Eliminating a signed vs. unsigned comparison.Tim King
2016-12-29Changing getTearDownIncremental() to return the type of ↵Tim King
options::tearDownIncremental.
2016-12-29Adding a destructor to InstantiationNotify.Tim King
2016-12-29Adding a destructor to RepBoundExt.Tim King
2016-12-29Reordering sep and sets in Makefile.theories.Tim King
2016-12-16Fix dependency tracing for fewerPreprocessingHolesAndres 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-14Switch from SMT-LIB v2.0 to v2.5 for smt2 filesAndres 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-14Made tear-down-incremental more like it used to be: when tear-down valueClark Barrett
is 1, it does not automatically enable incremental mode.
2016-12-11Merge branch 'master' into fix_orderClark Barrett
2016-12-11Merge pull request #116 from 4tXJ7f/fix_multClark Barrett
Fix (inactive) `MultSlice` rewrite
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback