Andrew Reynolds [Sat, 28 Oct 2017 18:01:49 +0000 (13:01 -0500)]
Sygus process conjecture (#1286)
* 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.
Andrew Reynolds [Sat, 28 Oct 2017 14:13:13 +0000 (09:13 -0500)]
Document term db (#1220)
* 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
Andrew Reynolds [Sat, 28 Oct 2017 04:16:38 +0000 (23:16 -0500)]
Improve strings rewriter for contains (#1207)
* 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.
Andrew Reynolds [Sat, 28 Oct 2017 00:21:18 +0000 (19:21 -0500)]
Document quant arith (#1271)
* Initial documentation, incomplete.
* Document arith utilities in quantifiers.
* Minor
* Clang format
* Minor
* Clang format.
* Minor
* Apply new clang format.
* Document ordering.
Andres Noetzli [Fri, 27 Oct 2017 21:01:35 +0000 (14:01 -0700)]
Modify LDFLAGS to support shared libraries for Win (#1280)
* 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
Andrew Reynolds [Fri, 27 Oct 2017 18:58:12 +0000 (13:58 -0500)]
Cbqi multiple instantiation (#1289)
* Multi-instantiation heuristic for cbqi bv.
* New clang format.
* Minor
* Minor.
* Minor
Andrew Reynolds [Fri, 27 Oct 2017 16:20:50 +0000 (11:20 -0500)]
Refactor theory model (#1236)
* 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.
Andrew Reynolds [Fri, 27 Oct 2017 14:03:07 +0000 (09:03 -0500)]
Implement Hilbert choice operator (#1291)
* Initial support for Hilbert choice operator.
* Clang format.
* Fix
* Minor
Tim King [Fri, 27 Oct 2017 03:13:25 +0000 (20:13 -0700)]
Adds a macro to SWIG to ignore the override and final C++11 keywords in older versions of SWIG. (#1281)
Andrew Reynolds [Thu, 26 Oct 2017 21:49:55 +0000 (16:49 -0500)]
Op overload no fun variant (#1285)
* Do not allow function variants with operator overloading.
* Minor.
* New clang format.
* Minor improvements.
Andres Noetzli [Thu, 26 Oct 2017 02:50:08 +0000 (19:50 -0700)]
Use uintptr_t for pointer casts in Swig files (#1278)
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.
Tim King [Thu, 26 Oct 2017 00:07:01 +0000 (17:07 -0700)]
Removing throw specifiers from OutputChannel and subclasses. (#1209)
Tim King [Wed, 25 Oct 2017 21:28:07 +0000 (14:28 -0700)]
Switching EqProof to use shared_ptr everywhere. (#1217)
This clarifies the memory ownership of EqProofs.
Aina Niemetz [Wed, 25 Oct 2017 20:04:05 +0000 (13:04 -0700)]
CBQI BV: Add handling for missing operators. (#1274)
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.
Andrew Reynolds [Wed, 25 Oct 2017 00:38:16 +0000 (19:38 -0500)]
Cbqi bv ineq mode (#1273)
* 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.
Andrew Reynolds [Tue, 24 Oct 2017 22:58:58 +0000 (17:58 -0500)]
Removing deprecated file. (#1270)
Mathias Preiner [Tue, 24 Oct 2017 20:46:05 +0000 (13:46 -0700)]
Remove clang-format options introduced in version 5.0.
Mathias Preiner [Tue, 24 Oct 2017 17:51:59 +0000 (10:51 -0700)]
New clang-format style based on the Google style. (#1264)
Aina Niemetz [Tue, 24 Oct 2017 05:46:50 +0000 (22:46 -0700)]
CBQI BV: Add ULT/SLT inverse handling. (#1268)
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.
Andrew Reynolds [Mon, 23 Oct 2017 19:43:20 +0000 (14:43 -0500)]
Document sygus programming-by-examples utility (#1260)
* 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
Mathias Preiner [Sat, 21 Oct 2017 04:03:04 +0000 (21:03 -0700)]
Add rewriting rules for Eq/Ult with sign_extend and constants. (#1258)
Mathias Preiner [Sat, 21 Oct 2017 02:01:51 +0000 (19:01 -0700)]
Simplify atoms introduced while bitblasting. (#1267)
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).
Andrew Reynolds [Fri, 20 Oct 2017 23:18:35 +0000 (18:18 -0500)]
SyGuS term size limit (#1262)
* Add option sygus-abort-size, which tells the enumerative SyGuS solver to abort when it reaches a given term size.
* Apply clang format.
Andrew Reynolds [Fri, 20 Oct 2017 19:52:31 +0000 (14:52 -0500)]
Make Sygus conjectures higher-order (#1244)
* 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.
Aina Niemetz [Thu, 19 Oct 2017 19:31:42 +0000 (12:31 -0700)]
CBQI BV: Refactor solve_bv_constraint. (#1265)
This refactors function solve_bv_constraint to use a switch-case over kinds rather than an if-else chain.
Andrew Reynolds [Wed, 18 Oct 2017 20:19:10 +0000 (15:19 -0500)]
Tptp unsat cores (#1228)
* Support unsat cores for TPTP.
* Fix assertion
Andrew Reynolds [Wed, 18 Oct 2017 17:11:50 +0000 (12:11 -0500)]
Strings API escape sequences (#1245)
* 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.
Tim King [Tue, 17 Oct 2017 23:01:21 +0000 (16:01 -0700)]
Making the values argument const in the SetUserAttributeCommand const… (#1249)
* Making the values argument const in the SetUserAttributeCommand constructor. Misc. cleanup of SetUserAttributeCommand.
* Removing override keyword that was making SWIG unhappy.
Tim King [Tue, 17 Oct 2017 20:17:20 +0000 (13:17 -0700)]
Fixing 2 instances of an unused variable. (#1253)
Clark Barrett [Tue, 17 Oct 2017 04:26:30 +0000 (21:26 -0700)]
Fix for issue 1247 (#1257)
* 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
Andrew Reynolds [Tue, 17 Oct 2017 00:21:25 +0000 (19:21 -0500)]
Sygus enumerators to conjecture (#1237)
* 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.
Tim King [Mon, 16 Oct 2017 18:22:21 +0000 (11:22 -0700)]
Adds unit test that show Node and TNode work with for each loops. (#1230)
Extends test/unit/expr/node_black.h with tests that show Node and TNode can work with C++11 for each loops.
Aina Niemetz [Fri, 13 Oct 2017 21:28:47 +0000 (14:28 -0700)]
CBQI BV: Added EXTRACT handling. (#1240)
This adds inverse handling for BITVECTOR_EXTRACT. Fixes previously disabled regressions. These regressions are now enabled.
Andrew Reynolds [Fri, 13 Oct 2017 05:12:02 +0000 (00:12 -0500)]
CBQI BV quick heuristics (#1239)
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.
Andrew Reynolds [Thu, 12 Oct 2017 19:07:05 +0000 (14:07 -0500)]
Initial support for solving bit-vector inequalities (#1229)
* 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
Andrew Reynolds [Thu, 12 Oct 2017 18:00:12 +0000 (13:00 -0500)]
Sygus logics (#1226)
* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions.
* Minor
* Add case for reals, comment.
* Fix regress1.
Aina Niemetz [Thu, 12 Oct 2017 05:20:17 +0000 (22:20 -0700)]
Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)
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.
Mathias Preiner [Thu, 12 Oct 2017 01:17:31 +0000 (18:17 -0700)]
Reduce number of travis builds.
This also removes the Java API test code, which will be tested in the nightly
builds. Same goes for the removed portfolio builds.
Mathias Preiner [Thu, 12 Oct 2017 00:58:33 +0000 (17:58 -0700)]
Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)
Tim King [Wed, 11 Oct 2017 23:01:32 +0000 (16:01 -0700)]
Cleaning up ProofArray class. (#1208)
Andrew Reynolds [Wed, 11 Oct 2017 16:42:23 +0000 (11:42 -0500)]
Ho Lambda Lifting (#1116)
* Do lambda lifting in term formula removal pass. Set option in SMT engine related to higher-order.
* Better documentation
Andrew Reynolds [Wed, 11 Oct 2017 13:51:05 +0000 (08:51 -0500)]
Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion to remove non-invertible operators. Add regression. (#1222)
Andrew Reynolds [Wed, 11 Oct 2017 11:11:46 +0000 (06:11 -0500)]
Move unsat core names to smt engine (#1192)
* 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
Andrew Reynolds [Wed, 11 Oct 2017 02:07:14 +0000 (21:07 -0500)]
Ho node manager types (#1203)
* Remove restrictions about function types
* Introduce notion of first-class type, improve assertions, add comment on equality type rule.
* Update comment
Aina Niemetz [Tue, 10 Oct 2017 22:36:09 +0000 (15:36 -0700)]
Add copyright information. (#1201)
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.
Andres Noetzli [Tue, 10 Oct 2017 21:45:36 +0000 (14:45 -0700)]
Fix memory leak in quantifiers engine (#1219)
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.
Martin [Tue, 10 Oct 2017 06:21:26 +0000 (07:21 +0100)]
Add skeleton of the FP theory solver (#1130)
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.
Andrew Reynolds [Tue, 10 Oct 2017 02:56:40 +0000 (21:56 -0500)]
Split term database (#1206)
* 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.
Aina Niemetz [Tue, 10 Oct 2017 00:06:30 +0000 (17:06 -0700)]
CBQI BV: Add inverse for more operators. (#1213)
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).
Clark Barrett [Thu, 5 Oct 2017 21:47:37 +0000 (14:47 -0700)]
Fix typo in comment.
Mathias Preiner [Thu, 5 Oct 2017 21:42:18 +0000 (14:42 -0700)]
Split COPYING file, add missing licenses. (#1195)
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
Andrew Reynolds [Thu, 5 Oct 2017 14:11:03 +0000 (09:11 -0500)]
Minor change to how SyGus commands are translated to SmtEngine commands. This ensures a single success is printed for synth-fun and synth-inv. (#1193)
Andrew Reynolds [Thu, 5 Oct 2017 12:12:47 +0000 (07:12 -0500)]
Ho model (#1120)
* Update model construction for higher order. If HO_APPLY terms are present for a function, we use a curried (tree) model construction to avoid exponential size model representations for function definitions.
* Update comments.
* Change terminology in comment.
* Improve comments.
Martin [Thu, 5 Oct 2017 09:08:53 +0000 (10:08 +0100)]
Allow CDHashMaps for objects without default constructors (#1092)
This is a patch, originally from mdeters/cdhashmap-default-constructibility that allows CDHashMaps to be declared for objects that don't have default constructors.
Aina Niemetz [Thu, 5 Oct 2017 03:40:11 +0000 (20:40 -0700)]
Add mkZero, mkOne and mkUmulo to bv utils. (#1200)
This adds several utility functions for the theory BV. Function mkUmulo encodes an unsigned multiplication overflow detection operation, which we need for CBQI BV. In the future, we will introduce a Umulo node kind (and a corresponding bit-blasting strategy based on the encoding implemented in mkUmulo).
Andrew Reynolds [Wed, 4 Oct 2017 23:54:45 +0000 (18:54 -0500)]
Ho quant util (#1119)
Quantifiers utilities for higher-order.
This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges.
Also adds required options and a minor utility for implementing app completion.
Tim King [Wed, 4 Oct 2017 16:26:28 +0000 (09:26 -0700)]
Removing the throw specifier from ArrayStoreAll constructor. (#1182)
Addresses CIDS:
1457252 and
1379620.
Miscellaneous cleanup to ArrayStoreAll.
Andrew Reynolds [Wed, 4 Oct 2017 03:39:36 +0000 (22:39 -0500)]
Add regression from #50 regarding "as" parsing in smt2 (#1188)
* Add regression from pull request #50, which was fixed separately in pull request #1162.
* Improve comment in regression
Mathias Preiner [Tue, 3 Oct 2017 23:09:38 +0000 (16:09 -0700)]
Add Cryptominisat and LFSC to --show-config output. (#1194)
Also removed obsolete CUDD related code.
Andrew Reynolds [Tue, 3 Oct 2017 15:19:27 +0000 (10:19 -0500)]
Move sygus grammar utilities to separate file. (#1184)
* Move sygus grammar utilities to separate file.
* Minor
* Move includes
Andrew Reynolds [Tue, 3 Oct 2017 12:05:28 +0000 (07:05 -0500)]
Op overload parser (#1162)
* Update parser for operator overloading.
* Improvements
* Updates
* Add assert
Andres Noetzli [Tue, 3 Oct 2017 07:55:35 +0000 (00:55 -0700)]
Add initial version of the SMTCOMP2018 run scripts (#1185)
This commit is a preparation step for removing the --thread-stack
option (and, ultimately, the dependency on Boost). It just copies the
2017 version of the scripts and changes the --fs-inst flag to
--fs-interleave, following the renaming in commit
7766f0ba088ad6d6c58ea9678477b255c9e52fee.
Andres Noetzli [Tue, 3 Oct 2017 05:48:00 +0000 (22:48 -0700)]
Unify hash functions for pairs (#1161)
CVC4 was implementing multiple, slightly different hash functions for
pairs. With pull request #1157, we have a decent generic hash function
for pairs. This commit replaces the existing hash function
implementations with a typedef of the generic hash function.
Martin [Tue, 3 Oct 2017 00:41:24 +0000 (01:41 +0100)]
Add 5 FP kinds for partial to total fn conversion (#1128)
- Add new kinds for partially defined functions
- Print the new kinds
- Type rules for the new total kinds
- Constant folding and rewrites for the new total kinds
Mathias Preiner [Mon, 2 Oct 2017 19:35:28 +0000 (12:35 -0700)]
Address comments from PR #1164. (#1174)
Make eliminateSkolemFunctions(...) iterative and some more minor fixes.
Tim King [Mon, 2 Oct 2017 16:11:49 +0000 (09:11 -0700)]
Removing throw specifiers from SymbolTable::Implementation. (#1183)
Tim King [Mon, 2 Oct 2017 05:05:49 +0000 (22:05 -0700)]
Removing throw specifiers from TypeEnumeratorBase's operator* and isFinished. (#1176)
The throw specifier has been moved to a comment.f
This allows for fixing several CIDs on FloatingPointEnumerator:
1457254,
1457258,
1457260,
1457269,
1457270,
1457274, and
1457275.
This also has miscellaneous formatting, documentation and const labeling improvements.
Tim King [Mon, 2 Oct 2017 02:12:12 +0000 (19:12 -0700)]
CID
1457268: Initializing CegConjecture::d_syntax_guided to false. (#1181)
Andrew Reynolds [Sun, 1 Oct 2017 16:57:52 +0000 (11:57 -0500)]
Refactor check function in last call effort of non-linear extension. (#1175)
Andrew Reynolds [Sat, 30 Sep 2017 11:35:12 +0000 (06:35 -0500)]
SyGuS streaming solution mode (#1131)
* Refactor conjecture class in ce guided instantiation, move to own file. In preparation for sygus streaming mode.
* Infrastructure for streaming guards, more cleanup.
* Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup.
* More cleanup, add comments.
* Update comments
* Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter.
* Fix makefile.
* Cleanup.
* Remove unused includes.
* Minor
Mathias Preiner [Fri, 29 Sep 2017 23:47:59 +0000 (16:47 -0700)]
Move BvInverter class into separate file. (#1173)
Clark Barrett [Fri, 29 Sep 2017 22:55:33 +0000 (15:55 -0700)]
A few updates to license files.
Andres Noetzli [Fri, 29 Sep 2017 21:43:19 +0000 (14:43 -0700)]
Add license information for GMP
Andrew Reynolds [Fri, 29 Sep 2017 19:28:52 +0000 (14:28 -0500)]
Simplify representation of inversion Skolems for bv cegqi (#1164)
* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.
* Enable other regression
Andrew Reynolds [Fri, 29 Sep 2017 12:23:22 +0000 (07:23 -0500)]
Initial working version of BV word-level instantiation (#1158)
* Initial work on BV CEGQI, still working on avoid circular dependencies with inversion skolems.
* Guard by option, minor notes.
* Minor
* Minor fixes.
* Minor
Andres Noetzli [Fri, 29 Sep 2017 08:14:51 +0000 (01:14 -0700)]
Better hash function for pairs (#1157)
CVC4 was computing hashes for pairs of objects by simply XORing the
hashes of the two objects. This commit implements a better way of
combining hashes based on the FNV-1a hash algorithm. The algorithm is
public domain.
Andrew Reynolds [Fri, 29 Sep 2017 04:58:03 +0000 (23:58 -0500)]
Update symbol table to support operator overloading (#1154)
Mathias Preiner [Fri, 29 Sep 2017 03:32:36 +0000 (20:32 -0700)]
Fix output of --show-config for readline. (#1159)
cvc4 --show-config reported the wrong configuration for readline since
HAVE_LIBREADLINE is set to 0 or 1 but was checked with #ifdef.
Andrew Reynolds [Thu, 28 Sep 2017 21:31:02 +0000 (16:31 -0500)]
Cegqi refactor prep bv (#1155)
* Preparing for bv instantiation, initial working version.
* Undoing bv changes to break up into smaller commit.
Andrew Reynolds [Thu, 28 Sep 2017 12:23:33 +0000 (07:23 -0500)]
Improve finite model finding for recursive predicates (#1150)
* Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions.
* Simplifications, update comments.
Andrew Reynolds [Wed, 27 Sep 2017 23:49:41 +0000 (18:49 -0500)]
Minor fixes for partial quantifier elimination. (#1147)
This forces "counterexample lemmas" (the formula B => ~phi[e] on page 23 of http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf) to be added during TheoryQuantifiers::preRegisterTerm instead of at full effort check. This is required to ensure that CVC4's partial quantifier elimination algorithm produces correct results.
Some background:
"get-qe" and "get-qe-disjunct" are commands in the SMT2 parser. Here is how they can be used:
[declarations]
[assertions A]
(get-qe (exists X F))
returns a ground formula F' such that A ^ F' and A ^ (exists X F) are equivalent.
The command "get-qe-disjunct" provides an interface for doing an incremental version of "get-qe".
[declarations]
[assertions A]
(get-qe-disjunct (exists X F))
returns a ground formula F1' such that A ^ F' implies A ^ (exists X F). It moreover has the property that if you call:
[declarations]
[assertions A]
(assert F1')
(get-qe-disjunct (exists X F))
this will give you a formula F2' where eventually:
[declarations]
[assertions A]
(assert (not (or F1' ... Fn')))
(get-qe-disjunct (exists X F))
will either return "true" or "false", for some finite n.
Here is an example that failed before this commit:
(set-logic LIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (or (not (>= (+ a (* (- 1) b)) 1)) (not (>= (+ c (* (- 1) d)) 0))))
(get-qe-disjunct (exists ((x Int)) (and (> a b) (> c x) (> d x))))
This should return:
(not (or (not (>= (+ a (* (- 1) b)) 1)) (>= (+ c (* (- 1) d)) 1)))
Previously it was returning:
false
This is because the cbqi algorithm needs to assume the negation of the quantified formula we are doing qe on before it makes any decision.
The get-qe-partial feature is being requested by Cesare and Daniel Larraz for Kind2.
This improves our performance on quantified LIA/LRA:
https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
see CVC4-092617-2-fixQePartial
Aina Niemetz [Wed, 27 Sep 2017 20:45:27 +0000 (13:45 -0700)]
CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)
This implements side conditions and the instantiation via word-level inversion for operator BITVECTOR_MULT.
Andrew Reynolds [Wed, 27 Sep 2017 11:50:47 +0000 (06:50 -0500)]
Add quantifiers API example, fixes #879 (#1146)
Andres Noetzli [Wed, 27 Sep 2017 07:43:30 +0000 (00:43 -0700)]
Fix seeking for buffered input (#1145)
CVC4's implementation of seek was calculating the pointer difference
between the current position in the input and the seek point to
determine how many characters to consume. This was causing problems when
ANTLR was seeking to a pointer on a line after the current line because
it would result in a big number of characters to consume because each
line is allocated separately. This resulted in issue #1113, where CVC4
was computing a large number of characters to consume and would block
until it received all of them. This commit fixes and simplifies the
code by simply consuming characters until the seek point is reached
without computing a count beforehand.
Martin Brain [Wed, 27 Sep 2017 03:00:17 +0000 (20:00 -0700)]
Fix type checking of to_real (#1127)
to_real takes a single argument as given in kinds.
Martin Brain [Wed, 27 Sep 2017 00:21:51 +0000 (17:21 -0700)]
Improve FP rewriter: const folding, other (#1126)
Tim King [Tue, 26 Sep 2017 20:02:32 +0000 (13:02 -0700)]
Fixing CIDs
1172014 and
1172013: Initializing members of GetProofCommand and GetModelCommand to nullptr. (#1142)
Tim King [Tue, 26 Sep 2017 18:26:40 +0000 (11:26 -0700)]
Fixing Cid
1172009 (#1141)
Tim King [Tue, 26 Sep 2017 16:36:52 +0000 (09:36 -0700)]
Fixing CID
1172020: Initializing CDHashMap::iterator::d_it to nullptr. (#1139)
Tim King [Tue, 26 Sep 2017 14:33:31 +0000 (07:33 -0700)]
Fixing CID
1362903: Initializing d_bvp to nullptr. (#1136)
Tim King [Tue, 26 Sep 2017 09:28:57 +0000 (02:28 -0700)]
CID
1362904: Initializing GetInstantiationsCommand::d_smtEngine to nullptr. (#1135)
Andres Noetzli [Tue, 26 Sep 2017 07:46:14 +0000 (00:46 -0700)]
Fix build for old GMP version (#1114)
Older versions of GMP in combination with newer versions of GCC and
C++11 cause errors [0]. This commit adds the necessary includes of
<cstddef>.
[0] https://gcc.gnu.org/gcc-4.9/porting_to.html
Tim King [Tue, 26 Sep 2017 06:51:42 +0000 (23:51 -0700)]
Fixing CIDs
1172012 and
1172011: Initiallzing d_exprManager to nullptr in const_iterator. (#1140)
Andrew Reynolds [Tue, 26 Sep 2017 00:43:27 +0000 (19:43 -0500)]
Cegqi refactor substitutions (#1129)
This refactors the apply substitution mechanism for counterexample-guided quantifier instantiation (CEGQI).
Improvements to the code:
(1) Methods have been added to the TermProperties class that summarize their theory-independent behavior (including "getModifiedTerm", "isBasic" etc.). For now, I have not made a "TermPropertiesArith" class yet since this will require more fundamental refactoring.
(2) The terminology "has_coeff" is replaced "is_non_basic" throughout.
(3) Added the applySubstitutionToLiteral method.
(4) Both applySubstitution and applySubstitutionToLiteral are now private within CegInstantiator. This means that theory-specific instantiators do not need to implement custom ways of applying substitutions (previously the arithmetic instantiator was).
(5) applySubstitutionToLiteral is automatically called on all literals (see line 297 of ceg_instantiator.cpp). This means that BvInstantiator::processAssertion is now called on substituted literals. So for instance if our context contains two literals:
x = bv2, bvmul(x,y) = bv4
Say we are asked to solve for x first, and return the substitution {x -> bv2}, then if we are later asked to solve for y, we will call processAssertion for the literal bvmul(bv2,y)=bv4
(6) LIA-specific information "d_theta" in SolvedForm is encapsulated inside the class (with the understanding that this will be made virtual).
This commit has no impact on quantified LIA / LRA: https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
(see CVC4-092217-cegqiRefactorSubs)
Tim King [Mon, 25 Sep 2017 23:06:14 +0000 (16:06 -0700)]
Initializing BVMinisat Solver::notify to nullptr. (#1132)
Andrew Reynolds [Mon, 25 Sep 2017 21:42:02 +0000 (16:42 -0500)]
Fix bug related to sort inference + subtypes. (#1125)
Tim King [Mon, 25 Sep 2017 20:02:48 +0000 (13:02 -0700)]
Fixing CID
1362917: There was a branch where d_issup was not initialized. Switching members of InstantiationEngine to uniqur_ptr to simplify such cases. (#1133)
Tim King [Mon, 25 Sep 2017 15:58:45 +0000 (08:58 -0700)]
Fixing CID
1362895: Initializing d_bvp to nullptr. (#1137)
* Fixing CID
1362895: Initializing d_bvp to nullptr. Miscellaneous cleanup.
Tim King [Mon, 25 Sep 2017 06:20:12 +0000 (23:20 -0700)]
CID
1362907: Initializing d_smtEngine to nullptr. (#1134)
Andrew Reynolds [Thu, 21 Sep 2017 08:20:09 +0000 (03:20 -0500)]
Sygus inv templ refactor (#1110)
* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.
* Update comment on class
* Cleanup
* Comments for sygus type construction.