summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Collapse)Author
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
C++11 introduced the thread_local keyword, so we don't need to use non-standard extensions or our custom pthread extension anymore. The behavior was previously introduced as a workaround in commit 753a072c542c1c254d7c6adbf10e091ba585ede5. This commit introduces the macro CVC4_THREAD_LOCAL that can be used to declare variables as thread local. For Swig, this macro is defined to be empty.
2017-08-25Move LFSC checker out of the CVC repository. (#222)Aina Niemetz
LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution anymore. As a consequence, we + Add --with-lfsc and --with-lfsc-directory as configure options. In the case where CVC4 has not been built with integrated LFSC, all code that interacts with LFSC is disabled. + Disable proof checking if CVC4_USE_LFSC is not defined. Configuring the build with --check-proofs but without --with-lfsc results in an error. + Do not call LFSC's cleanup function (but we should in the future). LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt. Disabled call to lfscc_cleanup until the problem in lfscc is fixed. + Disable building with LFSC for the distcheck travis build since it is not part of the distribution anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker before calling make check on the temp build (the build of the unpacked distribution tar ball).
2017-08-17Add mbqi interleave option, change option fs-inst to fs-interleave.ajreynol
2017-08-10Fix line numbers in options_templateAndres Noetzli
2017-08-04Set default language to smt lib 2.6 (including as a base language for ↵ajreynol
sygus), update regressions.
2017-07-14Removing BOOST_FOREACH usage.Tim King
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵ajreynol
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
2017-07-10Merge 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-07Update copyright headers.Mathias Preiner
2017-06-28Enable non-linear solve by default, update regressions.ajreynol
2017-05-30print only labeled assertions as part of the unsat coreguykatzz
added the option dump-unsat-cores-full for printing the entire core, as before
2017-05-12Adding VPATH back inmakaimann
2017-05-12Conditional coverage buildmakaimann
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is ↵ajreynol
on, add regression.
2017-04-21Handle subtypes in sets. Bug fixes for tuples with subtypes.ajreynol
2017-04-20Minor fixes.ajreynol
2017-04-18Coverage fixmakaimann
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-07Change option names for nl.ajreynol
2017-04-05Merge pull request #143 from FabianWolff/masterClark Barrett
Fix several spelling errors
2017-04-05Add 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-05Fix several spelling errorsFabian Wolff
2017-04-04Enable multi-trigger-linear by default, add option.ajreynol
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge ↵Tim King
commit for nlAlgMaster.
2017-03-31Add option multi-trigger-linear, minor optimization to E-matching.ajreynol
2017-03-29Add quantifiers options related to model and master equality engine.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-22Work on new approach for sygus involving conditional solutions. Refactoring ↵ajreynol
of sygus solver. Bug fix for sygus solution reconstruction.
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-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-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-15Minimization modes for fmf bound.ajreynol
2017-02-07Generalize finite bound inference to unifiable variables in set membership ↵ajreynol
literals.
2016-12-29Changing getTearDownIncremental() to return the type of ↵Tim King
options::tearDownIncremental.
2016-12-07Refactoring, 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-21Refactoring related to track instantiation option.ajreynol
2016-11-11Add simple inferences for extended bitvector functions, add a few related ↵ajreynol
options. Use bv2nat, int2bv as triggers. Add regressions.
2016-11-10Add option for enabling/disabling lazy extended function reduction in ↵ajreynol
bitvectors.
2016-11-08Add a few options to separation logic and sets. Minor changes to separation ↵ajreynol
logic, change syntax for empty heap constraint.
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ajreynol
as extension of sets solver, add regressions.
2016-10-05Added an option that allow empty dependencies when attempting to minimize ↵guykatzz
preprocessing holes
2016-09-20More refactoring of cbqi. Add a few regressions. Add option for qcf.ajreynol
2016-09-16Use matching heuristics for EPR instantiation.ajreynol
2016-09-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by ↵ajreynol
default in EPR mode.
2016-09-12Refactor prenex modes.ajreynol
2016-09-12Remove old implementation of cbqiajreynol
2016-09-09Support 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-03Option for prenex normal formajreynol
2016-09-01Fix boolean term issue in invariants from sygus. Minor default options ↵ajreynol
changes for cbqi.
2016-09-01Updates 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback