summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Collapse)Author
2018-01-14Removing throw specifiers from OptionsHandler. (#1510)Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-09Fix output of --trace=help. (#1500)Aina Niemetz
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
Removing more miscellaneous throw specifiers.
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-29Cbqi repeat solve literal (#1458)Andrew Reynolds
2017-12-27Disable sygus PBE when sygus stream is enabled (#1451)Andrew Reynolds
2017-12-20Transcendental functions check model (#1443)Andrew Reynolds
2017-12-10Add new infrastructure for preprocessing passes (#1053)justinxu421
This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).
2017-12-08Add CEGQI BV linearization of additions and equalities over additions. (#1417)Mathias Preiner
Adds support for linearizing additions w.r.t. to a variable. For example, a * x + b + c * d * -x = e + x is rewritten to x * (a - c * d - 1) = e - b. This also adds an additional rewriting rule x * x = x --> x < 2.
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-05Fix output of --show-trace-tags. (#1430)Mathias Preiner
Now prints each tag in a separate line.
2017-12-03Normalize grammars - 2 (#1420)Haniel Barbosa
This is another step towards addressing #1304 and #1344. This pull request: - Refactors SygusGrammarNorm - Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used. - Performs a "chain transformation" in the application of the PLUS operator in integer grammars - Removes redundant expansions of definitions from TermDbSygus - Adds a default empty print callback to SygusEmptyPrintCallback This lays the basis for more general linearizations.
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.
2017-11-29Minor improvements and changes to defaults for cbqi bv (#1406)Andrew Reynolds
This makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables. Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default Allows cbqiNestedQE to be used in the BV logic. Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-11-21Adding infrastructure for normalizing SyGuS grammars (#1397)Haniel Barbosa
* minor Using string previously computed * adding option * starting module for simplifying grammars * more * more * fix * fix * fix * fix * fix * removing unused command * removing unused command * removing unnecessary quantifier engine * adding lambda support * transient * reverting changes * starting normalization of integers * removing unnecessary objects * using for_each * rebuilding given datatypes * recrating types as given * bug fixing * minor * reverting space changes * addressing review * addressing review
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
* Preprocess extract -> concat pass for cegqi bv. * Add sygus bench * Fixes, infrastructure. * Minor fixes. * Try * Minor * Minor * Document * Format * Improving debug messages. * Address * Format * Overlapping extracts. * Format * Minor * Address review. * Format * Comment * Format
2017-11-18Ho instantiation (#1204)Andrew Reynolds
* Higher-order instantiation. * Add missing files. * Document inst match generators, make collectHoVarApplyTerms iterative. * More documentation. * More documentation. * More documentation. * More documentation * Refactoring, documentation. * More documentation. * Fix comment, reference issue. * More documentation. Fix ho trigger for the changes from master. * Minor * More documentation. * More documentation. * More * More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive. * More * Minor improvements to comments. * Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator. * Improve documentation for ho_trigger. * Update ho trigger to not access now private member of TermDb. * Address comments. * Address * Clang format
2017-11-17Add random number generator. (#1370)Aina Niemetz
This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).
2017-11-13Disable sygus qe preprocessing by default (#1353)Andrew Reynolds
* Disable qe preprocessing for sygus by default, add option. * Fix bug * Unnest one * Format
2017-11-03Fix bv help message. (#1315)Andrew Reynolds
2017-11-03Sygus clean main (#1297)Andrew Reynolds
* Remove front end hack for sygus. * Remove other hack, add sygus solution output mode. * Clang format * Minor * Fix * Minor * Remove unused field.
2017-10-27Cbqi multiple instantiation (#1289)Andrew Reynolds
* Multi-instantiation heuristic for cbqi bv. * New clang format. * Minor * Minor. * Minor
2017-10-24Cbqi bv ineq mode (#1273)Andrew Reynolds
* Add mode for cbqi bv inequality handling. * Implement the mode. * Clang format * Apply new clang format. * Revert "Apply new clang format." This reverts commit 1fec0ed999e45daacc4c756f11b5ecb4690f6561. * Revert "Clang format" This reverts commit 17042edb82d64c159aeddfe0264cd663998d0471. * Clang format, second try. * Revert "Clang format, second try." This reverts commit f862c47c34bc313f5bc49a26b7586a4824e5aae0. * Apply clang format, try 3.
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit.
2017-10-20SyGuS term size limit (#1262)Andrew Reynolds
* Add option sygus-abort-size, which tells the enumerative SyGuS solver to abort when it reaches a given term size. * Apply clang format.
2017-10-12CBQI BV quick heuristics (#1239)Andrew Reynolds
Adds two heuristics for cbqi-bv, both disabled by default. The first optimistically solves for boundary points of inequalities. The second randomly interleaves inversion and value instantiations. Adds some newly solved regressions from SMT LIB.
2017-10-10Add copyright information. (#1201)Aina Niemetz
This adds option --copyright which displays copyright information for CVC4. It further extends --show-config with copyright information and adds a banner with copyright information in interactive mode.
2017-10-04Ho quant util (#1119)Andrew Reynolds
Quantifiers utilities for higher-order. This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges. Also adds required options and a minor utility for implementing app completion.
2017-10-03Add Cryptominisat and LFSC to --show-config output. (#1194)Mathias Preiner
Also removed obsolete CUDD related code.
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
* Refactor conjecture class in ce guided instantiation, move to own file. In preparation for sygus streaming mode. * Infrastructure for streaming guards, more cleanup. * Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup. * More cleanup, add comments. * Update comments * Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter. * Fix makefile. * Cleanup. * Remove unused includes. * Minor
2017-09-29Initial working version of BV word-level instantiation (#1158)Andrew Reynolds
* Initial work on BV CEGQI, still working on avoid circular dependencies with inversion skolems. * Guard by option, minor notes. * Minor * Minor fixes. * Minor
2017-09-20Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)Andrew Reynolds
* Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms. * Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent. * Remove unused NodeList
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback