summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-07Guard relevant domain computation properly, minor. (#1325)Andrew Reynolds
2017-11-07 Removing an unused member from Tptp. Initializing members of Tptp. (#1326)Tim King
* Removing an unused member from Tptp. Initializing members of Tptp. * Removing delcaration for myPopCharStream.
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-07Allow FORALL in quantifier elimination command (#1322)Andrew Reynolds
* Allow FORALL passed as an argument to get-qe. * Document * Format * Minor
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-06Add getValue() for Rational and Integer (GMP and CLN). (#1309)Aina Niemetz
Returns a copy of d_value to enable public access of GMP and CLN data.
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-03Fix bv help message. (#1315)Andrew Reynolds
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-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 Add option to build shared Windows dependencies (#1282)Andres Noetzli
This commit adds an option to the contrib/get-win-dependencies script (-s) to build shared library versions of ANTLR and GMP, which enables building the shared versions of the CVC4 libraries needed for language bindings.
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-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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback