summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-03-30[Coverity] Remove throw qualifiers in src/smtremove_throwAndres Notzli
Addresses coverity issues: 1172167 1172174 1172176 1172183 1172185 1172186 1172188 1172189 1172191 1172192 1172193 1172194 1172197 1172197 1172198 1172434 1172437 1172438 1172443 1172445 1172446 1172447 1172448 1362695 1362700 1362717 1362736 1362768 1362786 1362811 1379599 1421404 1421405 1421406 1421407 1421408 1421409 1421410 1421411 1421412 1421413
2017-03-30Minor fixes for trigger selection max.ajreynol
2017-03-29Add quantifiers options related to model and master equality engine.ajreynol
2017-03-28Refactor the standard effort of relational solverPaul Meng
2017-03-28Fix bug 787.ajreynol
2017-03-28Fix for bug 733Clark Barrett
2017-03-28Minor refactoring sygus.ajreynol
2017-03-28More work on sygus. Add regress4 to Makefile.ajreynol
2017-03-27Fixing a bug for checking whether a node was visited.Tim King
2017-03-27Minor cleanups to ExtTheory.Tim King
2017-03-27Removing the friend class modifier from ExtTheory to Theory.Tim King
2017-03-27Merge pull request #137 from 4tXJ7f/throw_qualsClark Barrett
Remove throw qualifiers in type enumerators
2017-03-27Making the ExtTheory object a private member of Theory.Tim King
2017-03-27Making ppNotifyAssertions take a const vector.Tim King
2017-03-27Moving the CareGraph into its own file.Tim King
2017-03-27Moving the theory::Assertion struct into its own file.Tim King
2017-03-27Remove throw qualifiers in type enumeratorsAndres Notzli
This addresses Coverity issues: - 1172154 - 1172156 - 1172157 - 1172158 - 1172159 - 1379612 - 1379612 - 1421430 - 1172166 - 1172144 - 1362709 - 1362696 - 1172145 - 1172147 - 1172148 - 1379610 - 1362772 - 1362676 - 1362704 - 1362749 - 1362876 - 1362843 - 1362837 - 1362881 - 1172223 - 1172155
2017-03-26Alphabetizing libcvc4_la_SOURCES.Tim King
2017-03-24Add some regressions. Minor.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ↵ajreynol
Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
2017-03-23Fixing warning message.Clark Barrett
2017-03-23support incremental unsat coresguykatzz
2017-03-22Fix more cases of rewritten explanations in strings for bug 784. Minor.ajreynol
2017-03-22Minor fix for bounded integers.ajreynol
2017-03-22Work on new approach for sygus involving conditional solutions. Refactoring ↵ajreynol
of sygus solver. Bug fix for sygus solution reconstruction.
2017-03-21Improve computeCareGraph functions to check shared term equality status once ↵ajreynol
per equivalence class pair.
2017-03-20fixed cvc4 parser for set complementPaul Meng
2017-03-18Fix for bug 707.Clark Barrett
2017-03-18Fix to help with bug 717Clark Barrett
2017-03-17better 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-16Fixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.Tim King
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback