summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2018-01-05Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)Mathias Preiner
2018-01-03Global negate (#1466)Andrew Reynolds
2018-01-02Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)Aina Niemetz
We now can handle all cases of (in|dis)equality over BITVECTOR_UREM. This also simplifies some of the side conditions for equality.
2018-01-02Fix handling for UGT/SGT. (#1467)Mathias Preiner
Previously, we only handled the case x s < t. With this fix, we now get BITVECTOR_[SU]GT for litk if we encounter a literal t < x s.
2018-01-02Rewrites for BitVector multiplication (#1465)Andrew Reynolds
2017-12-29Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)Aina Niemetz
We now can handle all cases of (in|dis)equality over UREM. Previously, we could not handle equality for index=0 and had to rewrite x % s = t to x - x / s * s. Since we can now handle this case, we do not apply this rewriting anymore.
2017-12-28Fix unit tests for ineq for CBQI BV. (#1456)Aina Niemetz
2017-12-28Add unit tests for side conditions for inequality for CBQI BV. (#1455)Aina Niemetz
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-13Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441)Aina Niemetz
This adds side conditions for operators BITVECTOR_SHL, BITVECTOR_LSHR and BITVECTOR_ASHR for index = 1, i.e., s << x = t and s >> x = t. Previously, we treated these cases as non-invertible.
2017-12-10Fix issue 1433. (#1435)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-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-30Add debugging tools for ContextMemoryManager (#1407)Andres Noetzli
This commit adds two configuration options that help debugging memory issues with allocations in the ContextMemoryManager: --enable/disable-valgrind: This flag enables/disables Valgrind instrumentation of the ContextMemoryManager. Enabled by default for debug builds if the Valgrind headers are available. --enable/disable-context-memory-manager: This flag enables/disables the use of the ContextMemoryManager. If the flag is disableda dummy ContextMemoryManager is used that does single allocations instead of chunks. The flag is enabled by default.
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-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-15Adding garbage collection for Proof objects. (#1294)Tim King
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-09Add modular arithmetic operators. (#1321)Aina Niemetz
This adds functions on Integers to compute modular addition, multiplication and inverse. This is required for the Gaussian Elimination preprocessing pass for BV.
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-25Removing throw specifiers from OutputChannel and subclasses. (#1209)Tim King
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-16Adds unit test that show Node and TNode work with for each loops. (#1230)Tim King
Extends test/unit/expr/node_black.h with tests that show Node and TNode can work with C++11 for each loops.
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback