summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Collapse)Author
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2018-02-08Remove invalid regression test (#1579)Andres Noetzli
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-02-06Fix two multiply-by-constant corner cases for bv rewriter (#1562)Andrew Reynolds
2018-02-06Fix rewrite for string replace (#1537)Andrew Reynolds
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-02Fix remaining synthesis solution regressions (#1557)Andrew Reynolds
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
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-12Improvements for CBQI BV (#1504)Andrew Reynolds
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2018-01-03Global negate (#1466)Andrew Reynolds
2018-01-02Rewrites for BitVector multiplication (#1465)Andrew Reynolds
2017-12-27Rel smt parser (#1446)Arjun Viswanathan
2017-12-20Fixes for cbqi-bv (#1449)Andrew Reynolds
2017-12-20Add explicit disequality handling when generating side condition for CBQI ↵Aina Niemetz
BV. (#1447) This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.
2017-12-20Transcendental functions check model (#1443)Andrew Reynolds
2017-12-10Fix issue 1433. (#1435)Andrew Reynolds
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL, BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL. It refactors side condition generation for better readability and unit testing. It further adds unit tests for all side conditions we generate in order to check if they too weak or to restrictive (which may result in unsound behavior). This is achieved by checking the following two implications: not (exists x. s * x = t => SC) ... if sat, SC is too restrictive not (SC => exists x. s * x = t) ... if sat SC is too weak This simplifies to checking not (SC <=> exists x. s * x = t).
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-12-04Fix strings rewriter for strip constant endpoint reverse direction (#1424)Andrew Reynolds
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
This commit fixes two issues with reset-assertions: - pending pops were not done in SmtEngine, resulting in the following assertion failure: d_userLevels.size() == 0 && d_userContext->getLevel() == 1 - all definitions were erased on reset-assertion in an SMT2 file, leading to errors about undefined types
2017-12-01Refactor and generalize PBE strategies (#1410)Andrew Reynolds
2017-11-29Improve caching in term formula removal (#1398)Andrew Reynolds
2017-11-28Improve rewrite for string substr (#1337)Andrew Reynolds
2017-11-27Fix models for --solve-real-as-int. (#1371)Andrew Reynolds
2017-11-25Fixes for higher-order (#1405)Andrew Reynolds
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
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-15Reenable some regressions, minor. (#1369)Andrew Reynolds
2017-11-14Clean Ceg Instantiators (#1365)Andrew Reynolds
* Initial setup for preprocessing counterexample lemmas. * Improve documentation. * Improving documentation, infrastructure. * Extraction -> concatentation as a preprocess step. * Clang format * Minor * Make option, refactor effort levels. * Format * Clean * Format * Rename * Format * More * Format * Splitting changes. * Format * Revert option. * Minor * 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-13Argument Relevance for Synthesis Conjectures (#1311)Andrew Reynolds
* Initial work on conjecture-specific symmetry breaking. * More infrastructure, working on process term. * Flattening. * Process defs * More setup * Fixes. * Sketching * Generalize to inference of argument definitions. * More, separate conjunct processing per synth function. * Single occurrence variables. * Assign relevance. * Document, connecting. * Connecting to grammar construction. * Enabled, add regressions. * Fix regressions. * Clang format. * Add regress1, minor. * Fix * Two passes. * Fix * Note * Improve check match, make single var occurrence more conservative. * Add regression. * Clang format * Minor comments * Update regression to new option. * Undo grammar cons changes. * Enable irrelevant args. * Improvements. * Format * Minor
2017-11-05Improve rewriting for string contains part 2 (#1300)Andrew Reynolds
* Generalize component contains, some infrastructure. * Length entailment, substr for component contains, int.to.str for constant can contain concat. * Disable rewrite. * Fix, reenable length entailment for contains. * Clang format, minor. * Comment * Minor fixes and improvements for comments. * Improvements * Clang format * Fixes * Clang format * Fix, improve. * Format * Fix assertion
2017-11-03Suppport SAT logic (#1310)Andrew Reynolds
* Support SAT logic. * Add lustre example. * Add to smt1 as well. * Fix. * Fix. * Fix for new option.
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-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently. * Minor * Make unique bound variables for choice functions in BvInstantor, clean up. * Incorporate missing optimizations * Clang format * Unused field. * Minor * Fix, add regression. * Fix regression. * Fix bug that led to incorrect cleanup of instantiations. * Add missing regression * Improve handling of choice rewriting. * Fix * Clang format * Use canonical variables for choice functions in cbqi bv. * Add regression * Clang format. * Address review. * Clang format
2017-10-28Change bvudiv semantics based on input language (#1292)Andres Noetzli
* Change bvudiv semantics based on input language The semantics of division by zero have changed from SMT 2.5 to SMT 2.6. This commit sets the default options for the division semantics based on the language version used. The input language was already kept track of in the options, so this commit just updates the input language option when there is a set-info command. This mirrors how the code already deals with the output language. Note: With this commit, set-info overwrites the option set by the user. This is done to be consistent with the parser. This partially fixes #1241. * clang format
2017-10-27Improve strings rewriter for contains (#1207)Andrew Reynolds
* Work on rewriter for string contains. * Add rewrites that mix str.to.int and str.contains. Documentation, add regression. * Minor * Minor * Address review, add a few TODOs. Improve some non-digit -> not is number. * Fix * Simplify. * Clang format, minor fixing of comments.
2017-10-25CBQI BV: Add handling for missing operators. (#1274)Aina Niemetz
This adds inverse handling for BITVECTOR_XOR, BITVECTOR_SIGN_EXTENDS, BITVECTOR_COMP, BITVECTOR_ASHR. Function isInvertible() now corresponds to exactly the operators (plus index) for which we can determine an inverse, which avoids traversing along non-invertible paths. This further enables a test case that I missed to enable in PR #1268.
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-23Document sygus programming-by-examples utility (#1260)Andrew Reynolds
* Initial documentation and clean up of SyGuS PBE class, fix issue with concat strategy. * More documentation, cleanup. * Do not use concat strategy for 3+ arguments to concat, add regression. * Minor
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks. * Minor fix * Fix bug in Node::hasBoundVar for non-ground operators. * Add regression. * Address review. * Apply clang format.
2017-10-16Fix for issue 1247 (#1257)Clark Barrett
* Fix for bug 1247: in incremental mode, there was a corner case where a skolem variable introduced during ITE removal became a solved-for variable (part of the substitution map). But then if the same skolem was introduced again as part of a subsequent ITE removal pass, the substitution was not properly applied and an incorrect result was obtained. The handling of substitutions in incremental mode is quite kludgey - I opened an issue to revisit this. * fixing regression
2017-10-13CBQI BV: Added EXTRACT handling. (#1240)Aina Niemetz
This adds inverse handling for BITVECTOR_EXTRACT. Fixes previously disabled regressions. These regressions are now enabled.
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-12Initial support for solving bit-vector inequalities (#1229)Andrew Reynolds
* Initial support for solving bit-vector inequalities in cegqi-bv using conversion to positive equality + model value slack. * Clang format, remove heuristic. * Update regressions. * Simplify interface for CegInstantiator
2017-10-12Sygus logics (#1226)Andrew Reynolds
* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions. * Minor * Add case for reals, comment. * Fix regress1.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback