Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-07-10 | Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵ | ajreynol | |
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions. | |||
2017-07-10 | Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ | ajreynol | |
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions. | |||
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2017-06-28 | Enable non-linear solve by default, update regressions. | ajreynol | |
2017-05-30 | print only labeled assertions as part of the unsat core | guykatzz | |
added the option dump-unsat-cores-full for printing the entire core, as before | |||
2017-05-12 | Adding VPATH back in | makaimann | |
2017-05-12 | Conditional coverage build | makaimann | |
2017-05-05 | Do not eliminate extended arithmetic symbols when finite model finding is ↵ | ajreynol | |
on, add regression. | |||
2017-04-21 | Handle subtypes in sets. Bug fixes for tuples with subtypes. | ajreynol | |
2017-04-20 | Minor fixes. | ajreynol | |
2017-04-18 | Coverage fix | makaimann | |
Forcing some make variables to be absolute paths lcov does not (officially) support relative paths src/expr and src/options in particular were breaking it | |||
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 | 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-02 | Adding a model based axiom instantiation scheme for multiplication. Merge ↵ | Tim King | |
commit for nlAlgMaster. | |||
2017-03-31 | Add option multi-trigger-linear, minor optimization to E-matching. | ajreynol | |
2017-03-29 | Add quantifiers options related to model and master equality engine. | ajreynol | |
2017-03-24 | Refactor 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-22 | Work on new approach for sygus involving conditional solutions. Refactoring ↵ | ajreynol | |
of sygus solver. Bug fix for sygus solution reconstruction. | |||
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-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-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-15 | Minimization modes for fmf bound. | ajreynol | |
2017-02-07 | Generalize finite bound inference to unifiable variables in set membership ↵ | ajreynol | |
literals. | |||
2016-12-29 | Changing getTearDownIncremental() to return the type of ↵ | Tim King | |
options::tearDownIncremental. | |||
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. | |||
2016-11-21 | Refactoring related to track instantiation option. | ajreynol | |
2016-11-11 | Add simple inferences for extended bitvector functions, add a few related ↵ | ajreynol | |
options. Use bv2nat, int2bv as triggers. Add regressions. | |||
2016-11-10 | Add option for enabling/disabling lazy extended function reduction in ↵ | ajreynol | |
bitvectors. | |||
2016-11-08 | Add a few options to separation logic and sets. Minor changes to separation ↵ | ajreynol | |
logic, change syntax for empty heap constraint. | |||
2016-10-26 | New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ | ajreynol | |
as extension of sets solver, add regressions. | |||
2016-10-05 | Added an option that allow empty dependencies when attempting to minimize ↵ | guykatzz | |
preprocessing holes | |||
2016-09-20 | More refactoring of cbqi. Add a few regressions. Add option for qcf. | ajreynol | |
2016-09-16 | Use matching heuristics for EPR instantiation. | ajreynol | |
2016-09-15 | Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by ↵ | ajreynol | |
default in EPR mode. | |||
2016-09-12 | Refactor prenex modes. | ajreynol | |
2016-09-12 | Remove old implementation of cbqi | ajreynol | |
2016-09-09 | Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵ | ajreynol | |
allow sep disequal card constants when type is monotonic. Update logics on sep regressions. | |||
2016-09-03 | Option for prenex normal form | ajreynol | |
2016-09-01 | Fix boolean term issue in invariants from sygus. Minor default options ↵ | ajreynol | |
changes for cbqi. | |||
2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested ↵ | ajreynol | |
quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly. | |||
2016-08-31 | Removing typeof from didyoumean.cpp. | Tim King | |
2016-08-26 | Basic support for EPR+CBQI. Minor cleanup. | ajreynol | |
2016-08-25 | Options for counterexample guided instantiation. | ajreynol | |
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for ↵ | ajreynol | |
bounded set membership. | |||
2016-08-11 | Add support for fewer preprocessing holes | Andres Notzli | |
This commit adds support for the --fewer-preprocessing-holes flag. This flag changes the preprocessing part in proofs in two ways: it (1) removes assertions that are just restating inputs and uses the inputs directly instead and it (2) changes the form of the preprocessed assertions to contain the input that they originate from. The code in this commit is mostly taken from the proofs branch in Guy's fork. | |||
2016-07-27 | Added an option for a more aggressive weakest implicant optimization | Guy | |