Andres Noetzli [Thu, 3 May 2018 22:34:43 +0000 (15:34 -0700)]
Fix warnings in proof code (#1850)
Andrew Reynolds [Thu, 3 May 2018 19:23:48 +0000 (14:23 -0500)]
Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)
Andrew Reynolds [Thu, 3 May 2018 17:24:08 +0000 (12:24 -0500)]
Option to interleave tangent plane inferences (#1833)
Andrew Reynolds [Thu, 3 May 2018 16:30:09 +0000 (11:30 -0500)]
Link cegis unif with the enumeration manager (#1859)
Haniel Barbosa [Thu, 3 May 2018 12:54:27 +0000 (07:54 -0500)]
Make CegisUnif default to Cegis when no unif used (#1836)
Andrew Reynolds [Thu, 3 May 2018 06:16:08 +0000 (01:16 -0500)]
Fix cvc printer for nullary constructors (#1856)
Andres Noetzli [Thu, 3 May 2018 03:07:36 +0000 (20:07 -0700)]
Remove (dummy) SMT1 printer (#1854)
Andrew Reynolds [Thu, 3 May 2018 02:27:53 +0000 (21:27 -0500)]
Support HORN logic string (#1849)
Andrew Reynolds [Thu, 3 May 2018 01:25:09 +0000 (20:25 -0500)]
Initial support for string standard in smt lib 2.6 (#1848)
Andrew Reynolds [Tue, 1 May 2018 22:30:25 +0000 (17:30 -0500)]
Cegis unif enumerator manager (#1837)
Andrew Reynolds [Tue, 1 May 2018 15:47:40 +0000 (10:47 -0500)]
Improve tangent planes for transcendental functions (#1832)
Haniel Barbosa [Mon, 30 Apr 2018 20:33:21 +0000 (15:33 -0500)]
Refactor real2int (#1813)
This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass.
Andres Noetzli [Mon, 30 Apr 2018 19:17:13 +0000 (12:17 -0700)]
Remove dead code in bv-to-bool preprocessing pass (#1828)
Fixes Coverity issue
1468436. As Coverity correctly detects,
kind::BITVECTOR_XOR is dealt with in an if-statement before the switch
statement on kind. This is because kind::XOR is binary while
kind::BITVECTOR_XOR is n-ary (as a comment in the code correctly
indicates).
Andrew Reynolds [Mon, 30 Apr 2018 18:54:07 +0000 (13:54 -0500)]
Remove subsort symmetry breaking (#1807)
Andrew Reynolds [Mon, 30 Apr 2018 18:13:22 +0000 (13:13 -0500)]
Fix 1156 (#1830)
Andres Noetzli [Mon, 30 Apr 2018 17:52:11 +0000 (10:52 -0700)]
Disable unsat-cores/proofs for slow regression (#1835)
Andrew Reynolds [Mon, 30 Apr 2018 03:25:42 +0000 (22:25 -0500)]
Allow multiple functions in sygus unif approaches (#1831)
Andrew Reynolds [Mon, 30 Apr 2018 03:05:53 +0000 (22:05 -0500)]
Make factoring inference more aggressive (#1825)
Andrew Reynolds [Mon, 30 Apr 2018 02:43:51 +0000 (21:43 -0500)]
Refactor nonlinear check (#1814)
Andrew Reynolds [Mon, 30 Apr 2018 01:45:37 +0000 (20:45 -0500)]
Improvements to simple transcendental function check model. (#1823)
Haniel Barbosa [Sat, 28 Apr 2018 13:11:09 +0000 (08:11 -0500)]
Initial implementation of SygusUnifRL (#1829)
Andrew Reynolds [Sat, 28 Apr 2018 00:43:05 +0000 (19:43 -0500)]
Make construct solution behavior specific to SygusIO (#1827)
Andrew Reynolds [Fri, 27 Apr 2018 23:45:58 +0000 (18:45 -0500)]
Print function for equality status. (#1826)
Andrew Reynolds [Fri, 27 Apr 2018 20:03:31 +0000 (15:03 -0500)]
Simplify tangent plane direction (#1824)
Haniel Barbosa [Fri, 27 Apr 2018 19:33:01 +0000 (14:33 -0500)]
New module for synthesizing functions in a data-driven SyGuS approach (#1819)
Andrew Reynolds [Fri, 27 Apr 2018 18:55:08 +0000 (13:55 -0500)]
Core improvements to extended rewriter (#1820)
Andrew Reynolds [Thu, 26 Apr 2018 16:59:58 +0000 (11:59 -0500)]
Fix subgoal generation context (#1816)
yoni206 [Wed, 25 Apr 2018 22:12:51 +0000 (15:12 -0700)]
Refactor array-proofs and uf-proofs (#1655)
This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.
Andrew Reynolds [Wed, 25 Apr 2018 21:00:11 +0000 (16:00 -0500)]
Equality resolution in the extended rewriter (#1811)
yoni206 [Wed, 25 Apr 2018 18:54:23 +0000 (11:54 -0700)]
Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)
Andrew Reynolds [Wed, 25 Apr 2018 16:29:59 +0000 (11:29 -0500)]
Move candidate rewrite code to own file (#1804)
Andrew Reynolds [Wed, 25 Apr 2018 16:02:24 +0000 (11:02 -0500)]
Add benchmark requiring subgoal generation with induction. Disable option. (#1806)
Andrew Reynolds [Wed, 25 Apr 2018 14:53:41 +0000 (09:53 -0500)]
Remove nl solve subs option. (#1803)
Andrew Reynolds [Wed, 25 Apr 2018 14:28:22 +0000 (09:28 -0500)]
Fix issue with multi-triggers that include variable triggers (#1810)
Andrew Reynolds [Mon, 23 Apr 2018 20:11:44 +0000 (15:11 -0500)]
Draft smt comp 2018 for quantifiers and non-linear (#1808)
Andrew Reynolds [Sat, 21 Apr 2018 12:01:59 +0000 (07:01 -0500)]
Improve sygus sampling for strings (#1802)
Andres Noetzli [Sat, 21 Apr 2018 06:15:03 +0000 (23:15 -0700)]
Remove unused cache.h (#1795)
yoni206 [Fri, 20 Apr 2018 22:07:55 +0000 (15:07 -0700)]
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enabled (#1801)
Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable).
This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.
Andrew Reynolds [Fri, 20 Apr 2018 19:45:26 +0000 (14:45 -0500)]
Reenable filtering based on ordering in sygus sampler (#1784)
Andrew Reynolds [Fri, 20 Apr 2018 19:16:32 +0000 (14:16 -0500)]
Draft of casc j9 scripts (#1800)
yoni206 [Fri, 20 Apr 2018 17:26:50 +0000 (10:26 -0700)]
Allow metadata lines in test files to have leading spaces (#1799)
Currently, lines like `;EXPECT: sat` instead of `; EXPECT: sat` cause problems. This PR fixes it.
PaulMeng [Fri, 20 Apr 2018 15:15:00 +0000 (10:15 -0500)]
Symmetry detection module (#1749)
Andres Noetzli [Fri, 20 Apr 2018 12:53:32 +0000 (05:53 -0700)]
Restrict test summary to first-level subfolders (#1797)
yoni206 [Thu, 19 Apr 2018 22:42:39 +0000 (15:42 -0700)]
Adding config/tap-driver.sh to .gitignore (#1792)
#1791 removed config/tap-driver.sh from the repo, as ./autogen.sh adds it automatically.
The current PR prevents this file from being added to the untracked changes list when doing git status.
Andres Noetzli [Thu, 19 Apr 2018 18:47:38 +0000 (11:47 -0700)]
Refactor pbRewrites preprocessing pass (#1767)
This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.
Andres Noetzli [Thu, 19 Apr 2018 17:28:51 +0000 (10:28 -0700)]
Remove tap-driver.sh (#1791)
The autogen.sh script that we use causes the tap-driver.sh script to be
copied from automake installed on the system, so we do not have to
include it in our git repository. This also avoids ping-ponging between
different versions of the tap-driver script if different people have
different versions and commit them as part of their PRs.
Andres Noetzli [Tue, 17 Apr 2018 04:08:38 +0000 (21:08 -0700)]
Add timeout (option) to regression script (#1786)
This commit adds the option to run regressions with a timeout using the
`TEST_TIMEOUT` environment variable. The default timeout is set to 10
minutes. This should make it less likely that our nightly builds hang
and makes it easier to sort out slow tests.
Default timeout tested with regression level 2 on a debug build with
proofs.
Andres Noetzli [Tue, 17 Apr 2018 01:50:28 +0000 (18:50 -0700)]
Disable slow regression test (#1787)
Andres Noetzli [Mon, 16 Apr 2018 23:03:31 +0000 (16:03 -0700)]
Disable check proofs/unsat cores for two regs (#1785)
Disabling proof checking/unsat core checking for the two benchmarks in
question, reduces the time to run regressions significantly. After the
change, regression level 2 takes 7m30s to run on my machine and
regression level 1 takes just below 3m (16 threads). Individually, the
tests take over 7m each when checking proofs/unsat cores, so they add
significant overhead.
Andrew Reynolds [Mon, 16 Apr 2018 17:12:24 +0000 (12:12 -0500)]
Make 256 the default cardinality for strings (#1783)
Andres Noetzli [Mon, 16 Apr 2018 16:42:34 +0000 (09:42 -0700)]
RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)
Andrew Reynolds [Mon, 16 Apr 2018 13:14:53 +0000 (08:14 -0500)]
Skolemize candidate rewrite rule checks (#1777)
Andrew Reynolds [Mon, 16 Apr 2018 01:52:46 +0000 (20:52 -0500)]
Make strings fmf apply to all but internally generated Skolems (#1780)
Andrew Reynolds [Sun, 15 Apr 2018 18:58:21 +0000 (13:58 -0500)]
Fix type error with regexp (#1778)
Andrew Reynolds [Sun, 15 Apr 2018 15:18:34 +0000 (10:18 -0500)]
Fix mk type const (#1776)
This was a new utility, only used so far by the extended rewriter in EqChain simplification.
Andrew Reynolds [Sat, 14 Apr 2018 14:14:07 +0000 (09:14 -0500)]
Another fix for sygus rr stats. (#1768)
Andres Noetzli [Sat, 14 Apr 2018 09:27:44 +0000 (02:27 -0700)]
[Reg] Make status/unsat-core detection more robust (#1775)
This commit changes the regression script to look for status patterns or
get-unsat-core/get-unsat-assumption commands in the benchmark file
instead of the metadata file (i.e. the .expect file if it exists or the
benchmark file otherwise). This fix is not strictly necessary for our
current regressions but might have lead to surprising outcomes in the
future.
Andres Noetzli [Sat, 14 Apr 2018 08:28:17 +0000 (01:28 -0700)]
Fix get-unsat-core detection in regression script (#1773)
Due to a typo in the regression script, the (get-unsat-core) command was
not recognized (the script was looking for (get-unsat-cores)), so it
tried to run a regression script containing (get-unsat-core) even when
CVC4 was compiled without proof support. This commit fixes the typo.
yoni206 [Sat, 14 Apr 2018 05:58:37 +0000 (22:58 -0700)]
allowing --bool-to-bv without quantifiers (#1771)
Andres Noetzli [Sat, 14 Apr 2018 01:22:11 +0000 (18:22 -0700)]
Fix use-after-free in eager bitblaster (#1772)
There was a use-after-free in the eager bitblaster: the context used by
the SAT solver was destroyed before the solver. This lead to a
use-after-free in the destructor of the SAT solver when destroying
context-dependent objects. This commit fixes the issue by changing the
desctruction order such that the context is destroyed after the SAT
solver.
Note: This issue was introduced in commit
a917cc2ab4956b542b1f565abf0e62b197692f8d because d_nullContext and
d_satSolver were changed to be std::unique_ptrs.
Andrew Reynolds [Sat, 14 Apr 2018 00:38:17 +0000 (19:38 -0500)]
Disable split for negative contains. (#1774)
Andres Noetzli [Fri, 13 Apr 2018 22:53:44 +0000 (15:53 -0700)]
Fix issue in regression script when proofs enabled (#1770)
There were two issues in the new Python regression script when proofs
were enabled: It would try to run "--check-proofs" on SAT benchmarks and
the parameters added to check unsat cores were wrong. This commit fixes
both issues.
Andrew Reynolds [Fri, 13 Apr 2018 00:59:59 +0000 (19:59 -0500)]
Fix alpha equivalence for higher-order (#1769)
Andrew Reynolds [Thu, 12 Apr 2018 17:23:57 +0000 (12:23 -0500)]
Fixes for free variables in assertions (#1762)
Aina Niemetz [Wed, 11 Apr 2018 01:52:54 +0000 (18:52 -0700)]
Refactored BVGauss preprocessing pass. (#1766)
Andrew Reynolds [Wed, 11 Apr 2018 01:24:34 +0000 (20:24 -0500)]
Properly implement function extensionality based on cardinality (#1765)
Andrew Reynolds [Tue, 10 Apr 2018 21:44:02 +0000 (16:44 -0500)]
Improve accuracy of stats for sygus sampler (#1755)
Andres Noetzli [Tue, 10 Apr 2018 06:45:23 +0000 (23:45 -0700)]
Remove unused arith options (#1758)
Commit
629824db3911ab11ae286e4b14151a537602ba5a added options when
introducing the pseudo boolean processor that were never used. This
commit removes them.
Andrew Reynolds [Tue, 10 Apr 2018 02:18:19 +0000 (21:18 -0500)]
Fix hasSubterm calls for higher-order (#1760)
Aina Niemetz [Tue, 10 Apr 2018 01:50:39 +0000 (18:50 -0700)]
Fix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764)
Andrew Reynolds [Tue, 10 Apr 2018 01:09:51 +0000 (20:09 -0500)]
Fix higher-order term indexing. (#1754)
Andrew Reynolds [Mon, 9 Apr 2018 20:29:08 +0000 (15:29 -0500)]
Fix sygus substr static symmetry breaking (#1761)
Andres Noetzli [Sun, 8 Apr 2018 23:50:40 +0000 (16:50 -0700)]
Warn about trailing spaces in src/Makefile.am (#1759)
Andrew Reynolds [Sun, 8 Apr 2018 21:17:07 +0000 (16:17 -0500)]
Allow predetermined first-order variables when constructing deep embedding. (#1757)
Andrew Reynolds [Sun, 8 Apr 2018 20:23:20 +0000 (15:23 -0500)]
Check free variables in assertions (#1737)
Andrew Reynolds [Sun, 8 Apr 2018 20:01:52 +0000 (15:01 -0500)]
Do not introduce uinterpreted constants in TPTP parser (#1743)
Andrew Reynolds [Sun, 8 Apr 2018 19:36:20 +0000 (14:36 -0500)]
Add quantifier name attribute. (#1756)
Aina Niemetz [Sat, 7 Apr 2018 18:45:16 +0000 (11:45 -0700)]
Fixed get-authors.
Arjun Viswanathan [Fri, 6 Apr 2018 22:50:48 +0000 (17:50 -0500)]
Add define rec fun to cvc parser (#1738)
Andres Noetzli [Fri, 6 Apr 2018 04:45:17 +0000 (21:45 -0700)]
Python regression script (#1662)
Until now, we have been using a bash script for the running the
regressions. That script had several issues, e.g. it was creating many
temprorary files and it was calling itself recursively, making it
difficult to maintain. This commit replaces the script with a Python
script. The Python script uses the TAP protocol, which allows us to
display the results of multiple tests per file (e.g. with --check-models
and without) separately and with more details. It also outputs whenever it starts running
a test, which allows finding "stuck" regression tests on Travis. As recommended in the
automake documentation [0], the commit copies the TAP driver to enable
TAP support for the test driver.
Note: the commit also changes some of the regressions slightly because
we were using "%" for the test directives in SMT files which does not
correspond to the comment character ";". Using the comment character
simplifies the handling and makes it easier for users to reproduce a
failure (they can simply run CVC4 on the regression file).
[0]
https://www.gnu.org/software/automake/manual/html_node/Use-TAP-with-the-Automake-test-harness.html
Mathias Preiner [Thu, 5 Apr 2018 18:40:34 +0000 (11:40 -0700)]
Add more general SignExtendUltConst rewriting. (#1385)
This also adds an additional check in processAssertions to ensure that all
assertions are guaranteed to be rewritten (there was only a comment stating
this).
Andres Noetzli [Thu, 5 Apr 2018 18:06:26 +0000 (11:06 -0700)]
Make Python bindings example compatible w/ Python3 (#1751)
Andres Noetzli [Thu, 5 Apr 2018 05:43:48 +0000 (22:43 -0700)]
Update README for regression tests (#1746)
Andrew Reynolds [Wed, 4 Apr 2018 23:17:02 +0000 (18:17 -0500)]
Proper initialization and destruction of sygus unif (#1750)
Andrew Reynolds [Wed, 4 Apr 2018 21:17:35 +0000 (16:17 -0500)]
Fix for corner case of higher-order matching (#1708)
Andrew Reynolds [Wed, 4 Apr 2018 16:56:59 +0000 (11:56 -0500)]
Do not debug check models when unknown (#1748)
Andrew Reynolds [Wed, 4 Apr 2018 14:40:19 +0000 (09:40 -0500)]
Fix sygus infer (#1747)
Andres Noetzli [Wed, 4 Apr 2018 03:43:37 +0000 (20:43 -0700)]
Refactor IntToBV preprocessing pass (#1716)
This commit refactors the IntToBV preprocessing pass into the new style.
This commit is essentially just a code move, it does not attempt to fix
issues (e.g. #1715).
Andrew Reynolds [Wed, 4 Apr 2018 01:29:26 +0000 (20:29 -0500)]
Option to turn arbitrary input into sygus (#1704)
Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving.
This includes improvements to the robustness of the sygus solver.
Andres Noetzli [Wed, 4 Apr 2018 00:30:41 +0000 (17:30 -0700)]
[BVMiniSat] Avoid duplicates in conflicts (#1745)
If analyzeFinal() in BVMiniSat was called with a literal that also
occurred in the trail, it could happen that the set of assumptions that
led to the assignment of `p` contained `p` twice.
BitVectorProof::endBVConflict would then register that conflict with the
duplicate literal but at the same time compute a conflict expression
with the duplicate removed. LFSCSatProof::printAssumptionsResolution
would then output two resolutions for the same literal, which made the
simplify_clause side condition fail because it couldn't find the literal
in the clause anymore after the first removal.
The fix simply avoid adding `p` to the set of assumptions if it is found
in the trail. In this situation, `p` is guaranteed to be in the set of
assumptions already because it has been added at the beginning of
analyzeFinal(). This issue originally came up in PR #1384. With this fix
the regression tests pass in #1384.
Andrew Reynolds [Tue, 3 Apr 2018 23:13:04 +0000 (18:13 -0500)]
Make sygus unif I/O an subclass of sygus unif (#1741)
Andrew Reynolds [Tue, 3 Apr 2018 20:49:43 +0000 (15:49 -0500)]
Use choice when expanding definitions for inverse transcendental functions (#1742)
Andrew Reynolds [Tue, 3 Apr 2018 15:48:34 +0000 (10:48 -0500)]
Internal sygus type checking (#1734)
Andrew Reynolds [Tue, 3 Apr 2018 01:03:16 +0000 (20:03 -0500)]
Improvements to extended rewriter for Booleans and ITE (#1705)
Andrew Reynolds [Mon, 2 Apr 2018 22:50:31 +0000 (17:50 -0500)]
Make sygus unif utility use sygus unif strategies (#1732)
yoni206 [Mon, 2 Apr 2018 21:15:02 +0000 (14:15 -0700)]
a formula should be an instance of itself (#1668)
Proof checking failed when applying the instantiation rule so that the original formula and the instantiated formula are the same. Fixed using the new "ifequal" construct in lfsc.
Clark Barrett [Mon, 2 Apr 2018 20:35:24 +0000 (13:35 -0700)]
Remove references to nyu (#1721)
Mathias Preiner [Mon, 2 Apr 2018 19:48:44 +0000 (12:48 -0700)]
Reorganize bitblaster code. (#1695)
This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.
yoni206 [Mon, 2 Apr 2018 18:40:48 +0000 (11:40 -0700)]
Do not call toString() on malformed node when throwing TypeCheckingExceptionPrivate. (#1733)
While throwing a TypeCheckingExceptionPrivate, an IllegalArgumentException was thrown when
trying calling toString() on a malformed node. Fixed by printing the kind of the node and its children
rather than calling toString() on the malformed node.
Andrew Reynolds [Fri, 30 Mar 2018 19:26:28 +0000 (14:26 -0500)]
Disable regression (#1731)