summaryrefslogtreecommitdiff
path: root/src/options/quantifiers_options
AgeCommit message (Collapse)Author
2018-03-21Refactor mkoptions (#1631)Mathias Preiner
This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation. The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick. This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.
2018-02-27Improvements to sygus sampling (#1621)Andrew Reynolds
2018-02-08Minor improvements to sygus sampling. (#1577)Andrew Reynolds
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-04Sample based on sygus grammar by default (#1558)Andrew Reynolds
2018-02-02Option to use sampling for CEGIS (#1555)Andrew Reynolds
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
2018-02-01Use sygus to synthesize/verify rewrite rules (#1547)Andrew Reynolds
2018-01-22Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)Aina Niemetz
Previously, we computed an inverse for s1 o x, x o s2, s1 o x o s2 while disregarding that invertibility depends on si. This adds this handling as an optional heuristic for concats over (dis)equality since it improves performance on a considerable number of benchmarks.
2018-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
This refactors and simplifies solveBvLit() and fixes the following: - generate side conditions for BITVECTOR_NEG, BITVECTOR_NOT, BITVECTOR_PLUS, BITVECTOR_XOR over inequalities and disequality - fix CONCAT handling (generate side conditions rather then computing an inverse which was incorrect) - fix SIGN_EXTEND handling (same as with CONCATs)
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-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-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-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-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-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-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-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-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-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-08-17Add mbqi interleave option, change option fs-inst to fs-interleave.ajreynol
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-05-05Do not eliminate extended arithmetic symbols when finite model finding is ↵ajreynol
on, add regression.
2017-04-20Minor fixes.ajreynol
2017-04-04Enable multi-trigger-linear by default, add option.ajreynol
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-02-15Minimization modes for fmf bound.ajreynol
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-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.
2016-08-26Basic support for EPR+CBQI. Minor cleanup.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback