summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2017-11-09 Decouple sygus term database and term database. (#1317)Andrew Reynolds
* Decouple sygus term database and term database. * Clang format * Fix include
2017-11-07Initializing QModelBuilder members. (#1334)Tim King
2017-11-07Combining d_conflictHasBeenRaised and d_conflictIndex into a CDMaybe. (#1332)Tim King
2017-11-07Guard relevant domain computation properly, minor. (#1325)Andrew Reynolds
2017-11-07Moving the enum ArithType to partial_model. Adding a new type Unset in the ↵Tim King
enum. Always initializing VarInfo::d_type. (#1333)
2017-11-07Initializing EquivSygusInvarianceTest::d_conj in the constructor. (#1327)Tim King
2017-11-07Initializing NegContainsSygusInvarianceTest::d_cpbe in constructor. (#1328)Tim King
2017-11-06Using unique_ptr's for members of CegConjecture. (#1324)Tim King
2017-11-06Updates to interface for Sygus grammar construction. (#1323)Andrew Reynolds
* Updates to interface for grammar construction. * Minor * Format
2017-11-06Unrecurisify rewrite solve assertion for cbqi bv (#1312)Andrew Reynolds
* Unrecursify rewrite assertion for cbqi bv. * Format
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-05Make higher-order a flag in logic info. (#1318)Andrew Reynolds
* Make higher-order a flag in logic info. * Format * Minor * Format
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-01(Move-only) Split quant util (#1306)Andrew Reynolds
* Initial draft of splitting quant util. * Minor * Document recursive term builder. * Rename file, minor. * Clang format
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
* Fix some documentation. * Move model basis out of term db. * Moving * Finished moving. * Document Skolemize and term enumeration. * Minor * Model basis to first order model. * Change function name. * Minor * Clang format. * Minor * Format * Minor * Format * Address review.
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-11-01(Move-only) Refactor and document theory model part 2 (#1305)Andrew Reynolds
* Move type set to its own file and document. * Move theory engine model builder to its own class. * Working on documentation. * Document Theory Model. * Minor * Document theory model builder. * Clang format * Address review.
2017-10-31CID 1459592: Always checking whether rd is null or not. (#1299)Tim King
2017-10-30Remove include (#1298)Andrew Reynolds
2017-10-28(Move only) Move enumerative instantiation strategy to its own file and ↵Andrew Reynolds
document (#1290) * Move, document, and rename enumerative instantiation. * Clang format.
2017-10-28Sygus process conjecture (#1286)Andrew Reynolds
* Initial infrastructure for static preprocessing for sygus conjectures. * Initial infrastructure. * Minor change in terminology, move enumerator to synth-fun mapping to sygus term database, minor fix and add documentation to NegContainsInvarianceTest. * Clang format * Fixing comments, more initial infrastructure. * More * Minor * New clang format. * Address review.
2017-10-28Document term db (#1220)Andrew Reynolds
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206. * Minor * Minor * Change namespace style. * Address review * Fix incorrectly merged portion that led to regression failures. * New clang format, fully document relevant domain. * Clang format again. * Minor
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-27Document quant arith (#1271)Andrew Reynolds
* Initial documentation, incomplete. * Document arith utilities in quantifiers. * Minor * Clang format * Minor * Clang format. * Minor * Apply new clang format. * Document ordering.
2017-10-27Cbqi multiple instantiation (#1289)Andrew Reynolds
* Multi-instantiation heuristic for cbqi bv. * New clang format. * Minor * Minor. * Minor
2017-10-27Refactor theory model (#1236)Andrew Reynolds
* Refactor theory model, working on making RepSet references const. * Encapsulation of members of rep set. * More documentation on rep set. * Swap names * Reference issues. * Minor * Minor * New clang format.
2017-10-27Implement Hilbert choice operator (#1291)Andrew Reynolds
* Initial support for Hilbert choice operator. * Clang format. * Fix * Minor
2017-10-25Removing throw specifiers from OutputChannel and subclasses. (#1209)Tim King
2017-10-25Switching EqProof to use shared_ptr everywhere. (#1217)Tim King
This clarifies the memory ownership of EqProofs.
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-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-24Removing deprecated file. (#1270)Andrew Reynolds
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-20Add rewriting rules for Eq/Ult with sign_extend and constants. (#1258)Mathias Preiner
2017-10-20Simplify atoms introduced while bitblasting. (#1267)Mathias Preiner
If a newly introduced atom is not rewritten it can happen that the literals of both the original atom and the rewritten atom end up in the CNF. However, only the original atom has a BB definition and the literal of the rewritten atom is unconstrained (no BB definition).
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-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-19CBQI BV: Refactor solve_bv_constraint. (#1265)Aina Niemetz
This refactors function solve_bv_constraint to use a switch-case over kinds rather than an if-else chain.
2017-10-17Fixing 2 instances of an unused variable. (#1253)Tim King
2017-10-16Sygus enumerators to conjecture (#1237)Andrew Reynolds
* Initial revision of mapping sygus enumeration terms to CegConjectures. This will allow us to generalize conjecture-specific symmetry breaking. * Change function names, simplify. * Fix assertion, minor optimization * Cleanup, documentation, simplification. * Address review. * Apply clang format.
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-11Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)Aina Niemetz
This fixes and enables previously added regression tests for CBQI BV. It further removes one of the tests that was obsolete (since it goes through even without --cbqi-bv). This further fixes the inverse computation for BITVECTOR_LSHR, which was broken due to a mismatching bit-width when creating a shift node.
2017-10-11Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)Mathias Preiner
2017-10-11Cleaning up ProofArray class. (#1208)Tim King
2017-10-11Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ↵Andrew Reynolds
to remove non-invertible operators. Add regression. (#1222)
2017-10-10Ho node manager types (#1203)Andrew Reynolds
* Remove restrictions about function types * Introduce notion of first-class type, improve assertions, add comment on equality type rule. * Update comment
2017-10-10Fix memory leak in quantifiers engine (#1219)Andres Noetzli
Commit 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 introduced a memory leak where d_quant_attr was not deleted when the QuantifiersEngine was destroyed. This commit fixes the issue by turning d_quant_attr into an std::unique_ptr.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback