summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-27Modify LDFLAGS to support shared libraries for Win (#1280)Andres Noetzli
* Use uintptr_t for pointer casts in Swig files CVC4's Swig interface files were casting pointers to longs in multiple instances. The problem with that is that on certain platforms *cough* Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit executable (they use the LLP64 data model). This made the compilation of language bindings fail with MinGW. This commit changes the types to uintptr_t defined in Swig's stdint.i. * Modify LDFLAGS to support shared libraries for Win This commit adds "-no-undefined" to the LDFLAGS of CVC4's library, which is required for building DLLs (shared libraries on Windows). It also adds "--export-all-symbols" to the linker flags of the parser to ensure that there are no unresolved symbols when linking against it (see comment in the Makefile.am for details). * Fix for non-Windows builds * add no-undefined to libcvc4compatjni
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-26Adds a macro to SWIG to ignore the override and final C++11 keywords in ↵Tim King
older versions of SWIG. (#1281)
2017-10-26Op overload no fun variant (#1285)Andrew Reynolds
* Do not allow function variants with operator overloading. * Minor. * New clang format. * Minor improvements.
2017-10-25Use uintptr_t for pointer casts in Swig files (#1278)Andres Noetzli
CVC4's Swig interface files were casting pointers to longs in multiple instances. The problem with that is that on certain platforms *cough* Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit executable (they use the LLP64 data model). This made the compilation of language bindings fail with MinGW. This commit changes the types to uintptr_t defined in Swig's stdint.i.
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-24Remove clang-format options introduced in version 5.0.Mathias Preiner
2017-10-24New clang-format style based on the Google style. (#1264)Mathias Preiner
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-18Tptp unsat cores (#1228)Andrew Reynolds
* Support unsat cores for TPTP. * Fix assertion
2017-10-18Strings API escape sequences (#1245)Andrew Reynolds
* Argument for strings class to specify whether to process escape sequences. * Change default value on string constructor. * Make CVC4::String::toString symmetric to the constructor for CVC4::String, document. * Clang format.
2017-10-17Making the values argument const in the SetUserAttributeCommand const… (#1249)Tim King
* Making the values argument const in the SetUserAttributeCommand constructor. Misc. cleanup of SetUserAttributeCommand. * Removing override keyword that was making SWIG unhappy.
2017-10-17Fixing 2 instances of an unused variable. (#1253)Tim King
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-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-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.
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.
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-11Reduce number of travis builds.Mathias Preiner
This also removes the Java API test code, which will be tested in the nightly builds. Same goes for the removed portfolio builds.
2017-10-11Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)Mathias Preiner
2017-10-11Cleaning up ProofArray class. (#1208)Tim King
2017-10-11Ho Lambda Lifting (#1116)Andrew Reynolds
* Do lambda lifting in term formula removal pass. Set option in SMT engine related to higher-order. * Better documentation
2017-10-11Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ↵Andrew Reynolds
to remove non-invertible operators. Add regression. (#1222)
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand. * Comment * Pass expression names by reference. * Update throw specifiers. * Minor * Switch expression names to CDMap, simplify interface for printing unsat core names. * Revert throw specifier change. * Minor simplifcations
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-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-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.
2017-10-09Add skeleton of the FP theory solver (#1130)Martin
This commit adds the skeleton of the theory solver using a dummy version of the converter (fp_converter.{h,cpp}). The converter is a class that is used to produce bit-vector expressions equivalent to floating-point ones. The commit sets up the equality engine and the infrastructure for interacting with the main theory components. The majority of this code is still agnostic to how the conversion is actually implemented / what kind of theory solver this is. This is pretty much the template code you need to write any kind of theory solver. This includes equality reasoning and so should be able to solve some basic problems.
2017-10-09Split term database (#1206)Andrew Reynolds
* Move equality query to own file, move equality inference to quantifiers engine. * Move quantifiers attributes out of TermDb and into QuantAttribute. * Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header. * Split term database into term util. * Partial fix for #1205 that eliminates need for dependency in node.cpp. * Add more references to github issues.
2017-10-09CBQI BV: Add inverse for more operators. (#1213)Aina Niemetz
This implements side conditions and the instantiation via word-level inversion for operators BITVECTOR_AND, BITVECTOR_OR, BITVECTOR_UREM (Index=1), BITVECTOR_LSHR (index=0).
2017-10-05Fix typo in comment.Clark Barrett
2017-10-05Split COPYING file, add missing licenses. (#1195)Mathias Preiner
The COPYING file now only contains the modified BSD license of CVC4 and specifies the software that is either incorporated into CVC4 or can be linked against CVC4. The copyright and license information for each software can now be found in the licenses/<software>-LICENSE. The COPYING file has now 3 sections: (1) modified BSD license of CVC4 (2) non-GPLv3 software that is incorporated in CVC4 or that can be linked against CVC4 (3) GPLv3 software that can be optionally linked against CVC4
2017-10-05Minor change to how SyGus commands are translated to SmtEngine commands. ↵Andrew Reynolds
This ensures a single success is printed for synth-fun and synth-inv. (#1193)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback