Andrew Reynolds [Sun, 9 Aug 2020 21:50:09 +0000 (16:50 -0500)]
Splitting a few utility classes from EqualityEngine to their own file (#4862)
Includes iterators and notification callbacks. These classes will be highly relevant for planned extensions to the core theory engine infrastructure.
Andrew Reynolds [Sat, 8 Aug 2020 01:22:55 +0000 (20:22 -0500)]
Move datatype index constant to its own file (#4859)
Towards removing the Expr-level datatype.
Moves DatatypeIndex to its own file, which is the only thing that is necessary remaining from expr/datatype.h.
Also updates the datatype kinds file in preparation for the removal.
Aina Niemetz [Fri, 7 Aug 2020 21:56:28 +0000 (14:56 -0700)]
GH Actions: Remove cancel action. (#4843)
The previously introduced action to cancel running builds is not able to
cancel builds on other branches, only on the same branch. As a consequence,
when pushing to a branch for which a PR has been submitted, builds on the
main repository are not cancelled.
This removes the cancel build. If we want behavior similar to how it was
on Travis, we need a workaround / more sophisticated solution since GH
Actions doesn't really allow / support this (due to permission issues).
Andrew Reynolds [Thu, 6 Aug 2020 18:41:24 +0000 (13:41 -0500)]
Updates not related to creation for eliminating Expr-level datatype (#4838)
This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager.
This required updating a unit test from Expr -> Node.
Andrew Reynolds [Thu, 6 Aug 2020 13:29:17 +0000 (08:29 -0500)]
Split preprocessor from SmtEngine (#4854)
This splits a collection of utilities from SmtEngine that work in cooperation to preprocess assertions (Boolean circuit propagator, preprocessing context, process assertions, term formula removal).
It updates various interfaces in SmtEngine from Expr -> Node and simplifies SmtEngine to use this utility.
Andrew Reynolds [Thu, 6 Aug 2020 11:48:45 +0000 (06:48 -0500)]
(proof-new) Refactor regular expression operation (#4596)
This refactors the regular expression operation class so that some of its key methods are static, so that they can used by both the regular expression solver and the strings proof checker.
Notice that many cases of regular expression unfolding are deleted by this PR, since they are unnecessary. This is due to the fact that all regular expression memberships are rewritten except those whose RHS are re.++ or re.*.
Andrew Reynolds [Wed, 5 Aug 2020 19:14:23 +0000 (14:14 -0500)]
Split Assertions from SmtEngine (#4788)
This splits all things related to storing assertions in the SmtEngine into a separate class "Assertions". It also converts the interface for its methods from Expr to Node.
Gereon Kremer [Wed, 5 Aug 2020 18:55:00 +0000 (20:55 +0200)]
Improve error message for unsupported exponents (#4852)
We have had a few issues where essentially users misinterpreted the error message about which types of exponents are supported for (^ base exp). Given that this is rewritten to a multiplication of length exp, we only support reasonably small natural numbers.
This PR improves the error message.
Fixes #4692
Andrew V. Jones [Wed, 5 Aug 2020 17:38:15 +0000 (18:38 +0100)]
When checking models, ensure that error message is correctly formatted (#4853)
Issue
When CVC4 is checking models and encounters an issue, it presents an message like this:
Internal error detectedTHEORY_ARITH has an asserted fact that the model doesn't satisfy.
Notice: there's no space between detected and THEORY_ARITH.
Resolution
This PR ensures that the error message is correctly formatted.
Signed-off-by: Andrew V. Jones andrew.jones@vector.com
Andres Noetzli [Wed, 5 Aug 2020 14:18:10 +0000 (07:18 -0700)]
[Strings] Add eager context-dependent evaluation (#4847)
This commit adds eager evaluation of string terms based on the current
context. To do so, it declares the string kinds to be "interpreted" in
the equality engine. This allows us to avoid making a series of
decisions such as:
** (= "describe" (str.substr actionName 0 8)) :DE-DECISION:
*** (= actionName "deletecertificate") :DE-DECISION:
**** (= resource_partition "aws") :DE-DECISION:
***** (= resource_region "af-south-1") :DE-DECISION:
****** (= resource_account "") :DE-DECISION:
******* (= (str.len (str.substr actionName 0 3)) 0) :DE-DECISION:
******** (= (str.len (str.substr actionName 0 4)) 0) :DE-DECISION:
********* (= (str.len (str.substr actionName 0 6)) 0) :DE-DECISION:
********** (= (str.len (str.substr actionName 0 5)) 0) :DE-DECISION:
*********** (= (str.len (str.substr actionName 0 9)) 0) :DE-DECISION:
************ (= (str.len (str.substr actionName 0 7)) 0) :DE-DECISION:
************* (= (str.len (str.substr actionName 0 10)) 0) :DE-DECISION:
************** (= (str.len (str.substr actionName 0 2)) 0) :DE-DECISION:
*************** (= (str.len (str.substr actionName 0 13)) 0) :DE-DECISION:
**************** (= (str.len (str.substr actionName 0 12)) 0) :DE-DECISION:
***************** (= (str.len resource_service) 0) :DE-DECISION:
****************** (= (str.len resource_account) 0) :DE-DECISION:
In such a case, we can detect that there is a conflict after the first
two decisions because (str.substr "deletecertificate" 0 8) is
deletece which is different from describe. The equality engine uses
the rewriter to evaluate interpreted kinds with constant arguments.
This technique leads to a significant speedup on some of the newer
Amazon benchmarks.
Gereon Kremer [Wed, 5 Aug 2020 02:32:10 +0000 (04:32 +0200)]
Add dummy returns if libpoly is unavailable. (#4845)
This PR adds dummy return statements do CadSolver in case libpoly is not available.
Andrew Reynolds [Tue, 4 Aug 2020 23:27:27 +0000 (18:27 -0500)]
Fixes for getInterpolant and getAbduct API methods (#4846)
This fixes three issues in the getInterpolant method in the API, which was also copied to the getAbduct method:
(1) Use Node not Expr
(2) Must set up ExprManager scope
(3) The wrong solver pointer was passed to the returned term, which was causing segfaults on all abduction regressions.
We should also consider changing the interface of this method to return the term instead of a Boolean. This could be done as future work.
This fixes regress1.
Mathias Preiner [Tue, 4 Aug 2020 21:03:36 +0000 (14:03 -0700)]
Add documentation and build instructions for recompilation (LGPL). (#4844)
Abdalrhman Mohamed [Tue, 4 Aug 2020 20:23:54 +0000 (15:23 -0500)]
Modify the smt2 parser to use the Sygus grammar. (#4829)
Andrew Reynolds [Tue, 4 Aug 2020 19:01:47 +0000 (14:01 -0500)]
Add API interface for specialized constructor term (#4817)
This is an interface to get the instantiated parametric datatype constructor operator to apply when the type of this operator cannot be inferred without a cast.
This is required for eliminating the Expr-level datatype and calls to ExprManager from the parsers.
Gereon Kremer [Tue, 4 Aug 2020 11:32:21 +0000 (13:32 +0200)]
Properly initialize d_fullyInited. (#4840)
Fixed #4839.
The Boolean flag d_fullyInited is not properly initialized and is thus flagged by --ubsan.
Gereon Kremer [Tue, 4 Aug 2020 10:57:34 +0000 (12:57 +0200)]
Add CAD-based solver (#4834)
Based on #4774, this PR adds a new CadSolver class that allows the NonlinearExtension to actually employ the CAD-based method. In more detail:
add --nl-cad option
add CadSolver class that wraps cad::CDCAC with support for checks, model construction and conflict generation
add new Inference types for the NlLemma class
use CadSolver in NonlinearExtension (if --nl-cad is given)
Andres Noetzli [Mon, 3 Aug 2020 23:26:42 +0000 (16:26 -0700)]
Update documentation for Solver::mkVar() (#4833)
The documentation of `Solver::mkVar()` was not very clear regarding what
it could be used for. This lead to some confusion (see e.g. #4828).
This commit makes the documentation more explicit.
Ying Sheng [Mon, 3 Aug 2020 23:26:08 +0000 (16:26 -0700)]
Add implementation for SyGuS interpolation module (step4) (#4811)
This is the 4th step of adding interface for SyGuS Interpolation module. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
The 4th step finished the implementation of the interpolation module.
yoni206 [Mon, 3 Aug 2020 22:28:29 +0000 (15:28 -0700)]
New BV rewrite rules aimed at bv_to_int preprocessing pass (#4769)
This PR adds new rewrite rules for BV.
None of them is meant to be used by the default BV rewriter.
However, they are planned to be used in bv_to_int preprocessing pass.
In the pass we use FixpointRewriteStrategy to call various rewrite rules.
After consulting @4tXJ7f , we thought that the best way to include more rewrite rules in that call is to implement them using the existing BV rewrites infrastructure.
Andrew Reynolds [Mon, 3 Aug 2020 22:05:35 +0000 (17:05 -0500)]
Generalize interface for candidate rewrite database (#4797)
This class will be used as a utility in a new algorithm for solution reconstruction and requires a generalized interface.
FYI @abdoo8080
Andrew Reynolds [Mon, 3 Aug 2020 21:35:19 +0000 (16:35 -0500)]
Update datatypes in cvc parser to the new API (#4826)
This is leftover from the parser conversion. This is towards eliminating all remaining Expr-level calls in the parser.
Notice that 2 parser-level checks for records are eliminated in this PR, since we do not export record objects in the new API.
yoni206 [Mon, 3 Aug 2020 21:02:35 +0000 (14:02 -0700)]
Examples for using sygus python api (#4822)
This PR adds examples for using the sygus python api.
The examples are obtained from the examples of the cpp sygus api.
makaimann [Mon, 3 Aug 2020 20:39:44 +0000 (13:39 -0700)]
Delete solver pointer in Cython __dealloc__ (#4799)
Andrew Reynolds [Mon, 3 Aug 2020 18:42:17 +0000 (13:42 -0500)]
Split expression names from SmtEngine (#4832)
Towards splitting SmtEngine / deleting SmtEnginePrivate.
Andrew Reynolds [Mon, 3 Aug 2020 14:40:52 +0000 (09:40 -0500)]
Split dump manager from SmtEngine (#4824)
Towards splitting SmtEngine.
This moves utilities related to managing information for dumping to its own utility, DumpManager.
Its current responsibilities are to track information about how to print a model, and the implementation of some dumping traces, although its responsibilities should be extended further so that SmtEngine is not responsible for any command dumping. This is future work.
Andrew Reynolds [Sun, 2 Aug 2020 13:50:57 +0000 (08:50 -0500)]
Updates to dtype constructor in preparation for eliminating Expr-level datatype (#4825)
Andres Noetzli [Sun, 2 Aug 2020 12:57:24 +0000 (05:57 -0700)]
Fix ASan failure in interactive_shell_black (#4827)
This commit fixes an issue reported by ASan for unit test
interactive_shell_black. The unit test was failing because nodes were
created in the wrong node manager. The issue was likely introduced with
e8bbee7.
Andres Noetzli [Sun, 2 Aug 2020 06:56:27 +0000 (23:56 -0700)]
Ensure strict length constraint for decompose rule (#4821)
Fixes #4820. The performance issue was caused by
0988217562006d3f59e01dc261f39121df6d75f5. That commit introduced an
option (`--strings-len-conc`) that optionally moves the length
constraint for skolems to the conclusion of an inference instead of
making it part of the term registration. However, for
`DEQ_DISL_STRINGS_SPLIT`, we were only asserting that `LENGTH_GEQ_ONE`
in the case where this option was not enabled, instead of asserting that
the length of the skolem is equal to the component on the other side of
the disequality. This lead to an infinite loop of inferences because we
effectively were just splitting a component into two skolems and the
only restriction was that the first one was non-empty. We guessed the
second skolem to be empty, so the first skolem was equal to the
component, the skolem was marked congruent, and we ended up with the
same normal form as before.
The commit fixes the issue by adding an argument to
`getDecomposeConclusion()` that specifies whether to add the length
constraint or not. This option is used to always add the length
constraint in the case of `DEQ_DISL_STRINGS_SPLIT`.
Andrew Reynolds [Sun, 2 Aug 2020 03:27:08 +0000 (22:27 -0500)]
Add methods for constructing datatype types from NodeManager (#4823)
This is work towards eliminating the Expr-level datatype.
This PR implements the required methods for constructing datatype types from NodeManager.
In particular, this PR copies the "mkMutualDatatypeTypes" methods and converts them to Node-level.
The next PRs will be in preparation for using these methods instead of the Expr-level ones.
It also adds a flag d_isRecord to DType, which is required for supporting record printing in the cvc printer, which will be updated in another PR.
It also eliminates an interface for constructing constructor types via Expr-level DatatypeConstructor objects, which was unused.
Andrew V. Jones [Sat, 1 Aug 2020 07:34:37 +0000 (08:34 +0100)]
Ensure that we only find '.a's when building statically (#4785)
## Issue
When trying to building statically, and if your machine *does not* have static libraries (e.g., there is [no static GMP on CentOS 8](https://access.redhat.com/documentation/en-us/red_hat_enterprise_linux/8/html-single/considerations_in_adopting_rhel_8/index#removed-packages_changes-to-packages)), then CVC4's CMake does not detect this:
```
FAILED: bin/cvc4
: && /usr/bin/c++ -O3 -Wall -Wno-deprecated -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -Wno-class-memaccess -fuse-ld=gold -static src/main/CMakeFiles/main.dir/command_executor.cpp.o src/main/CMakeFiles/main.dir/interactive_shell.cpp.o src/main/CMakeFiles/main.dir/signal_handlers.cpp.o src/main/CMakeFiles/main.dir/time_limit.cpp.o src/main/CMakeFiles/cvc4-bin.dir/driver_unified.cpp.o src/main/CMakeFiles/cvc4-bin.dir/main.cpp.o -o bin/cvc4 src/libcvc4.a src/parser/libcvc4parser.a src/libcvc4.a -Wl,-Bdynamic /usr/lib64/libgmp.so -Wl,-Bstatic ../deps/install/lib/libantlr3c.a && :
/usr/bin/ld.gold: error: cannot mix -static with dynamic object /usr/lib64/libgmp.so
```
## Resolution
This PR changes CVC4's CMakeLists such that, if you're building statically, it *only* allows for linking against `.a`s (or `.a`s + `.lib`s on Windows).
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
Andrew Reynolds [Sat, 1 Aug 2020 07:20:24 +0000 (02:20 -0500)]
Fix component contains for splicing due to substring. (#4705)
Fixes #4701. That benchmark now times out.
yoni206 [Sat, 1 Aug 2020 06:50:40 +0000 (23:50 -0700)]
Add SyGuS Python API (#4812)
This commit extends the Python API with support for SyGuS functionality.
This required the addition of a nullary constructor for `Grammar` in the C++ API.
A unit test is also included, and is a translation of the corresponding C++ API unit test.
Examples are not added yet, but are ready and planned for a next PR (in order to keep this one shorter).
Andrew Reynolds [Fri, 31 Jul 2020 12:19:35 +0000 (07:19 -0500)]
Split listener classes from SmtEngine (#4816)
This moves listener classes owned by SmtEngine to their own file.
The SmtEnginePrivate class previously what itself a NodeManagerListener. This class will be deleted. Instead a new NodeManagerListener is introduced here whose sole responsibility is to do the work required for node manager listening.
Note I had to add a (temporary) friend relationship to SmtEngine, which will be removed in an upcoming PR to split the management of dumping to its own utility.
Andrew Reynolds [Fri, 31 Jul 2020 00:35:22 +0000 (19:35 -0500)]
Standardize explanations in arrays (#4804)
Some internal inferences had a non-standard way of providing (disjunctive) reasons and a custom way of explaining them.
This PR simplifies the array solver so that its explanations are analogous to the other equality engine based theory solvers (strings, datatypes, sets, ...). This is done in preparation for the incorporation of the proof equality engine in arrays, which follows a standard design for reasons/explanations.
The performance impact on QF arrays is negligible
Andres Noetzli [Thu, 30 Jul 2020 23:56:33 +0000 (16:56 -0700)]
Python API: Add support for sequences (#4757)
Commit
9678f58a7fedab4fc061761c58382f4023686108 added front end support
for sequences. This commit extends that support to the Python API. It
also adds simple C++ and Python examples that demonstrate how the API
works for sequences.
Gereon Kremer [Thu, 30 Jul 2020 21:59:40 +0000 (23:59 +0200)]
Cad implementation (#4774)
This commit implements the CAD interface added in #4773.
Gereon Kremer [Thu, 30 Jul 2020 16:16:25 +0000 (18:16 +0200)]
Adds the interface for the CAD-based arithmetic solver. (#4773)
This PR adds some utilities and, most importantly, the interface of the new
CAD-based solver.
The approach is based on https://arxiv.org/pdf/2003.05633.pdf and the code
structure follows the paper rather closely.
Andrew V. Jones [Thu, 30 Jul 2020 15:51:42 +0000 (16:51 +0100)]
When linking Editline, use 'pkg-config' to correctly find the link-time dependencies (#4809)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
Andrew Reynolds [Thu, 30 Jul 2020 14:54:57 +0000 (09:54 -0500)]
Fix null case for sygus printing (#4793)
Avoids crashing on some of our debug traces.
Andrew Reynolds [Thu, 30 Jul 2020 14:18:06 +0000 (09:18 -0500)]
(proof-new) Stream output for ProofNode (#4789)
Andrew Reynolds [Thu, 30 Jul 2020 01:15:44 +0000 (20:15 -0500)]
(proof-new) Fixes for getFreeAssumptions (#4802)
Free assumptions weren't getting cleaned up due to not doing a postorder traversal. This issue came up when doing subproof sharing involving SCOPE proofs.
Ying Sheng [Tue, 28 Jul 2020 22:35:06 +0000 (15:35 -0700)]
fixing issue #4808. (#4810)
fixing issue #4808. Remove structural binding, which only supported by c++17.
Andrew Reynolds [Tue, 28 Jul 2020 21:02:41 +0000 (16:02 -0500)]
Remove arrays lazy rintro option (#4806)
This option has model soundness issues (#4771) and moreover is overall worse performance on SMT-LIB {QF_ABV QF_ABVFP QF_ABVFPLRA QF_ALIA QF_ANIA QF_AUFBV QF_AUFLIA QF_AUFNIA QF_AX}:
Configuration #unsat time #sat time #solved #total
CVC4-072720_def 9428 9405.46 24932 16631.6 34360 35399
CVC4-072720_nalr1 9446 9536.41 24924 16146.3 34370 35399
where def = default, nalr1 = --no-arrays-lazy-rintro1.
Fixes #4771.
FYI @barrettcw
Andres Noetzli [Tue, 28 Jul 2020 18:59:28 +0000 (11:59 -0700)]
Replace Expr with Node in Term/Op (#4781)
This commit changes Term and Op to use Nodes internally instead of
Exprs. This is a step towards removing the Expr-layer. This commit also
adds some missing checks regarding the number of arguments for a given
kind that were previously missing, which caused issues in unit tests when
using Node instead of Expr.
Andrew Reynolds [Tue, 28 Jul 2020 18:25:40 +0000 (13:25 -0500)]
Fix regular expression delta for complement (#4765)
Fixes #4759 .
Also refactors this method.
yoni206 [Tue, 28 Jul 2020 17:44:55 +0000 (10:44 -0700)]
Supporting seq.nth (#4723)
This PR adds support for seq.nth operator by eliminating it during expandDefinitions, based on sub-sequences.
Tests that use this operator are also included.
Ying Sheng [Tue, 28 Jul 2020 16:55:52 +0000 (09:55 -0700)]
Interpolation: Add interface for SyGuS interpolation module (step3) (#4726)
This is the 3rd step of adding interface for SyGuS Interpolation module. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
The 3rd step partially implemented the interpolation module.
Andrew Reynolds [Tue, 28 Jul 2020 16:03:33 +0000 (11:03 -0500)]
Use lemma property enum for OutputChannel::lemma (#4755)
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
Andrew Reynolds [Mon, 27 Jul 2020 20:33:12 +0000 (15:33 -0500)]
(proof-new) Proof production for term formula removal (#4687)
This adds proof support in the term formula removal pass.
It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.
Andrew Reynolds [Mon, 27 Jul 2020 19:44:49 +0000 (14:44 -0500)]
(proof-new) Arithmetic operator elim proof producing (#4783)
This updates the interface for arithmetic operator elimination for the new proof format.
The actual proof production of the operator elimination class (providing proofs for
introduced witness terms) will be done in a separate PR.
This also changes the witness terms introduced by this class so their body is in
Skolem form, which simplifies term formula removal.
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Alex Ozdemir [Mon, 27 Jul 2020 17:20:07 +0000 (10:20 -0700)]
Consider negation's proof before triggering arith pfs. (#4776)
The current arith proof machinery can prove conflicts which are
explained by assumptions and tightened assumptions.
Previously we verified that the conflict constraint was explained in
terms of assumptions and tightened assumptions, before trying to
save/produce a proof.
We did not verify that the negated constraint was an assumption or
tightened assumption.
This caused us to attempt to prove conflicts around constraints whose
negations where proven by general means (in the case of #4714, by the
equality engine), which the proof machinery was not prepared to handle.
This PR also checks that the negate constraint is an assumption or
tightened assumption, before saving the proof.
Thanks, Gereon, for doing the initial investigation into this!
fixes 4714
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
Aina Niemetz [Tue, 21 Jul 2020 17:50:54 +0000 (10:50 -0700)]
GH Actions: Cancel builds on push, remove redundant mac OS build. (#4779)
Andrew Reynolds [Tue, 21 Jul 2020 16:15:39 +0000 (11:15 -0500)]
Support uninterpreted constants in the evaluator (#4777)
Gereon Kremer [Tue, 21 Jul 2020 13:28:38 +0000 (15:28 +0200)]
Preparations for a CAD-based arithmetic solver (#4762)
Based on #4679, this PR contains further preparations for a CAD-based arithmetic solver that extends the current NonlinearExtension.
In detail, it provides:
a Constraints class that manages all (polynomial) constraints visible to the cad solver,
a collection of methods used for cad projections,
a VariableOrdering class that provides different variable ordering heuristics tailored to cad,
an extension to the NlModel class, allowing for witness terms,
further conversion methods, in particular between Node and poly::Polynomial, poly::Value and RealAlgebraicNumber.
Alex Ozdemir [Mon, 20 Jul 2020 20:21:06 +0000 (13:21 -0700)]
Fix a deadlock in the signature tests. (#4772)
* wait() deadlocks if the OS pipe fills
* communicate() does not
This is essentially a duplicate of [this](https://github.com/CVC4/LFSC/pull/38).
Haniel Barbosa [Sat, 18 Jul 2020 05:20:19 +0000 (02:20 -0300)]
Improving equality engine tracing (#4770)
To keep track of the reasoning in the equality engine for n-ary kinds, for which partial applications amount to valid fully-applied terms, it's imperative to be able to see the IDs of the internal representation of the equality engine nodes. This commit updates tracing messages to print these IDs. It also improves the tracing for explanation generation.
Andrew Reynolds [Sat, 18 Jul 2020 04:16:18 +0000 (23:16 -0500)]
(proof-new) Proof recording for assertions pipeline (#4766)
Adds explicit steps to preprocess proof generator if one is provided.
Andrew Reynolds [Sat, 18 Jul 2020 02:24:22 +0000 (21:24 -0500)]
Enumerate shapes feature in fast sygus enumerator (#4742)
This adds the feature of enumerating shapes in the fast sygus enumerator, which is required for a new algorithm for sygus solution reconstruction.
This also adds a builtinToSygus backwards mapping that is required for that algorithm as well.
Note this also changes the implementation of mkFreeVar in sygus term database from skolem to bound variable, which is required to do proper caching for expr::hasBoundVar.
Andres Noetzli [Fri, 17 Jul 2020 22:25:54 +0000 (15:25 -0700)]
Add NodeManagerScopes to fix use-after-free issues (#4768)
This commit fixes our current ASan issues. Some methods in `NodeManager`
were not creating a `NodeManagerScope` for `this` but were indirectly
calling methods that get the `NodeManager` from the current scope, so we
ended up calling methods on a `NodeManager` that had already been
destroyed.
Andrew Reynolds [Fri, 17 Jul 2020 18:38:50 +0000 (13:38 -0500)]
Replace options listener infrastructure (#4764)
This replaces the old options listener infrastructure with the OptionsManager introduced in
cb8d041.
It eliminates a "beforeSearchListener", which was a custom way of some options throwing a modal exception if they were set after initialization. Now all options are consistent: no option can be set after initialization.
It also moves managed ostream objects to the OptionsManager.
@mpreiner The next step will be to remove the "notifies" field from the Options build system and then proceed with cleaning src/options/.
Andrew V. Jones [Fri, 17 Jul 2020 17:09:14 +0000 (18:09 +0100)]
Support for using 'libedit' over 'readline' #4571 (#4579)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
Andrew Reynolds [Fri, 17 Jul 2020 14:40:56 +0000 (09:40 -0500)]
(proof-new) Updates to strings core solver (#4642)
This updates the core strings solver in preparation for proofs.
The main changes include:
The addition of the strings PfRule enum values.
The definition of a "getConclusion" static method, used by the core solver, and to be used in the future by the strings proof checker. This includes several optional forms of lemmas, which are added as options in this PR.
Major simplifications to our inference schemas for disequality handling (a STRING_DECOMPOSE inference rule). Note this is the only significant intended behavioral change in this PR.
Minor updates to the form of inferences send to inference manager, for instance to orient equalities in the expected way, and to reorder assumptions. These changes are done for uniformity and make the strings proof reconstruction from inference steps easier.
Andrew Reynolds [Fri, 17 Jul 2020 12:35:14 +0000 (07:35 -0500)]
Add option manager and simpler option listener (#4745)
This adds the "OptionManager" class, which will live in SmtEngine. This is the required infrastructure for implementing all "reactive" options, i.e. those that must take effect immediately.
This PR does not enable this class yet, it simply adds the definitions.
After this PR, we can connect it to SmtEngine and delete the old options listener infrastructure.
Gereon Kremer [Fri, 17 Jul 2020 07:06:31 +0000 (09:06 +0200)]
Integration of libpoly (#4679)
This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration.
Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities.
Haniel Barbosa [Fri, 17 Jul 2020 02:23:05 +0000 (23:23 -0300)]
Fix EqProof to ProofNode conversion (#4760)
A wrong change slipped away during the cleaning of the module. This commit fixes the conversion.
Haniel Barbosa [Thu, 16 Jul 2020 21:52:15 +0000 (18:52 -0300)]
(proof-new) Implements the conversion between EqProof and ProofNode (#4756)
Gereon Kremer [Thu, 16 Jul 2020 19:57:36 +0000 (21:57 +0200)]
Resource manager cleanup (#4732)
This PR performs some general cleanup in and around the ResourceManager class. In detail, it does
remove --hard-limit (we decided to always leave the solver in a usable state, i.e. always do a soft limit),
remove --cpu-time (we decided to always use wall-clock time for time limiting)
replace old gettimeofday-based Timer by new std::chrono-based WallClockTimer
clean up the logic around beginCall() and endCall()
Andrew Reynolds [Thu, 16 Jul 2020 19:00:59 +0000 (14:00 -0500)]
Split abstract values utility from SmtEngine (#4754)
Towards refactoring SmtEngine.
Andrew Reynolds [Thu, 16 Jul 2020 17:10:58 +0000 (12:10 -0500)]
Make ExtTheory a utility and not a member of Theory (#4753)
Previously, we assumed that ExtTheory, the module for doing context-dependent simplification, was one-to-one with Theory. This design is not necessary. This makes this class a utility, which can be used as needed. This makes e.g. the initialization of TheoryStrings much easier, since the ExtTheory object can be created first.
Gereon Kremer [Thu, 16 Jul 2020 14:33:58 +0000 (16:33 +0200)]
Remove cumulative time limits and cpu time limits (#4711)
This PR removes two things from the resource manager:
cumulative time limits
cpu time limits
Cumulative time limiting has been moved to the binary and is (as before) accessible via --tlimit. As per discussion among the devs, we no longer support time limits based on CPU time and thus everything related to that is removed as well.
Note that this includes the option --cpu-time, removes an argument from SmtEngine::setTimeLimit() and the method SmtEngine::getTimeRemaining() .
Gereon Kremer [Thu, 16 Jul 2020 04:34:14 +0000 (06:34 +0200)]
Fixes memory leak when an exception goes through runCvc4(). (Fixes #4590) (#4750)
As noted in #4590, CVC4 may leak memory if an exception is thrown that interrupts the command execution loop in runCvc4().
While not a major issue (the binary is terminated anyway in this case, this is also why we label it as feature), we should fix it nevertheless.
This commit makes sure that the current command is properly managed by using `std::unique_ptr` to handle its deletion.
Haniel Barbosa [Thu, 16 Jul 2020 00:40:01 +0000 (21:40 -0300)]
(proof-new) Adding API for converting EqProof into ProofNode (#4747)
Also puts EqProof into its own module. Next will come the implementation of the API.
Andres Noetzli [Wed, 15 Jul 2020 23:42:00 +0000 (16:42 -0700)]
Use Nodes for SmtEngine assertions (#4752)
This commit changes SmtEngine::assertFormula() to use Nodes rather
than Exprs and changes AssertionList to be Node-based. This is
work towards removing the Expr layer.
Andrew Reynolds [Wed, 15 Jul 2020 18:30:23 +0000 (13:30 -0500)]
Split abduction solver from SmtEngine (#4733)
This splits everything related to abducts into its own standalone module, AbductionSolver.
It furthermore converts some of the interfaces of SmtEngine to make them take Node instead of Expr (this will be done for every method eventually).
The code for interpolation should follow a similar pattern, e.g. InterpolantSolver.
Andres Noetzli [Wed, 15 Jul 2020 15:27:13 +0000 (08:27 -0700)]
Use TypeNode in UninterpretedConstant (#4748)
This commit changes UninterpretedConstant to use TypeNode instead of
Type.
Gereon Kremer [Wed, 15 Jul 2020 11:15:24 +0000 (13:15 +0200)]
Add missing header (Fixes #4743) (#4749)
Thanks to Dejan for this hint (in #4743)
Andrew Reynolds [Wed, 15 Jul 2020 08:58:54 +0000 (03:58 -0500)]
Simplify entailment check interface (#4744)
The generality of this interface is unnecessary.
Andrew Reynolds [Tue, 14 Jul 2020 20:10:51 +0000 (15:10 -0500)]
Make use of options in setDefaults more consistent (#4729)
The plan is to make setDefaults (the method to update the default options based on our internal heuristics) modify an explicit copy of options.
This is the first step, which eliminates the dependence of this method on SmtEngine.
This PR is furthermore required to eliminate options listeners.
Andrew Reynolds [Tue, 14 Jul 2020 19:12:18 +0000 (14:12 -0500)]
Remove sygus print callback (#4727)
This removes sygus print callbacks, since they are no longer necessary to support the sygus v1 parser.
This involved generalizing the scope of the datatype utility sygusToBuiltin. Now, printing "as sygus" simply is accomplished by doing sygusToBuiltin conversion and then calling the printer on the builtin term.
This is required for further work towards eliminating the Expr layer.
FYI @4tXJ7f
Andrew Reynolds [Tue, 14 Jul 2020 18:08:45 +0000 (13:08 -0500)]
Fix regression output. (#4741)
This regression output was unexpected previously since conflict-based instantiation caught a conflict early, this makes it so that the output of this regression should be deterministic.
Fixes regress1.
Andrew Reynolds [Tue, 14 Jul 2020 16:30:47 +0000 (11:30 -0500)]
(proof-new) Skeleton proof support in the Rewriter (#4730)
This adds support for skeleton proofs in the rewriter (REWRITE -> THEORY_REWRITE).
It adds "extended equality rewrite" as a new method of the rewriter/theory rewriters.
The unit test of this feature should be added on a followup PR.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Andres Noetzli [Tue, 14 Jul 2020 14:33:01 +0000 (07:33 -0700)]
Use TypeNode in EmptySet (#4740)
This commit changes EmptySet to use TypeNode instead of Type.
Andrew Reynolds [Tue, 14 Jul 2020 06:41:24 +0000 (01:41 -0500)]
Debug instantiations output (#4739)
This prints # instantiations per round (during solving) for each quantified formula with `--debug-inst`, giving output like this:
```
(num-instantiations myQuant1 1)
(num-instantiations myQuant2 1)
unsat
```
It also changes the default value of print-inst-full to match the behavior of unsat-cores vs unsat-cores-full (by default, nameless quantifiers are ignored).
It fixes an issue with qid, where mkVar was accidentally used instead of mkConst, leading to assertion failures in debug. Marking major since this fixes debug regress1.
Andrew Reynolds [Tue, 14 Jul 2020 06:00:00 +0000 (01:00 -0500)]
Minor refactoring of subsolver initialization (#4731)
This decouples asserting a formula with initialization (previously it was a complex process to assert a formula due to having to clone/export to a new ExprManager). Now it is trivial.
This commit fixes an unintended consequence of the previous complications. Previously, SmtEngine::setOption would be set after asserting formulas to an SmtEngine subsolver, which is technically incorrect, as options should be finalized before the first assert.
This is required for further cleaning up of options listeners.
Andres Noetzli [Tue, 14 Jul 2020 05:11:10 +0000 (22:11 -0700)]
Fix caching in TheoryEngine::getExplanation() (#4736)
Commit
64a7db86206aa0993f75446a3e7f77f3c0c023c6 introduced a caching
mechanism in `TheoryEngine::getExplanation()`. However, there seem to be
issues related to the timestamps of the explanations. This commit fixes
the issue by making the timestamp part of the cache. The change ensures
that explanations for a certain node never rely on other explanations
for that node with a later timestamp.
Haniel Barbosa [Tue, 14 Jul 2020 03:53:39 +0000 (00:53 -0300)]
Fix options messages that were inverted (#4734)
Andres Noetzli [Tue, 14 Jul 2020 02:48:07 +0000 (19:48 -0700)]
Use TypeNode/Node in ArrayStoreAll (#4728)
This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.
Andrew Reynolds [Tue, 14 Jul 2020 01:52:02 +0000 (20:52 -0500)]
Fix type comparisons involving pointer. (#4738)
Fixes debug regressions, introduced by a combination of the addition of sequence update and the change to pointers.
Andrew Reynolds [Tue, 14 Jul 2020 00:53:25 +0000 (19:53 -0500)]
Fix whitespace issue in instantiations output. (#4737)
Fixes regress1.
Andrew Reynolds [Mon, 13 Jul 2020 22:42:57 +0000 (17:42 -0500)]
(proof-new) SMT Preprocess proof generator (#4708)
This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.
It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.
Andrew Reynolds [Mon, 13 Jul 2020 21:12:29 +0000 (16:12 -0500)]
User-facing print debug option for sygus candidates (#4720)
This makes an option --debug-sygus available to the user for tracing the sygus solver. For the classic max2 example the option is:
(sygus-enum 0)
(sygus-candidate (max 0))
(sygus-enum 0)
(sygus-enum 1)
(sygus-enum x)
(sygus-enum x)
(sygus-candidate (max x))
(sygus-enum x)
(sygus-enum y)
(sygus-enum y)
(sygus-candidate (max y))
(sygus-enum y)
(sygus-enum (+ x x))
(sygus-enum (+ x 1))
(sygus-enum (+ 1 1))
...
(sygus-enum (ite (<= x y) y 1))
(sygus-candidate (max (ite (<= x y) y 1)))
(sygus-enum (ite (<= x y) y 1))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-candidate (max (ite (<= x y) y x)))
unsat
(define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
Where sygus-enum denotes enumerated terms and sygus-candidate is one that passes a CEGIS refinement check.
Andrew Reynolds [Mon, 13 Jul 2020 19:21:47 +0000 (14:21 -0500)]
Statistics on instantiations per quantified formula. (#4719)
This adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).
It also simplifies and improves printing of Instantiation Tries.
Gereon Kremer [Mon, 13 Jul 2020 11:57:41 +0000 (13:57 +0200)]
Implement --tlimit for windows (#4716)
The new mechanism for --tlimit only works for POSIX compatible systems (that implement setitimer). This PR implements an alternative (though roughly equivalent) approach for windows, based on SetWaitableTimer().
To make this work (without code duplication) we need to call the timeout_handler function from time_limit.cpp as the windows solution employs an asynchronous callback instead of signals. I used the opportunity to rename util.cpp to signal_handlers.cpp (as it really does not do anything else) and reformat the file.
As I do not have a windows system at hand, I have not been able to actually test this apart from making sure that it compiles with the mingw setup.
Andrew Reynolds [Mon, 13 Jul 2020 05:43:45 +0000 (00:43 -0500)]
Add support for string/sequence update (#4725)
This adds basic support for string/sequence updating, which has a semantics that is length preserving.
Andres Noetzli [Mon, 13 Jul 2020 00:37:03 +0000 (17:37 -0700)]
Remove ExprSequence (#4724)
Now that we can break the old API, we don't need an ExprSequence
anymore. This commit removes ExprSequence and replaces all of its uses
with Sequence. Note that I had to temporarily make sequence.h public
because we currently include it in a "public" header because we still
generate the code for Expr::mkConst<Sequence>().
Andrew Reynolds [Sat, 11 Jul 2020 12:45:35 +0000 (07:45 -0500)]
Cache explanations in TheoryEngine::getExplanation (#4722)
For some hard verification benchmarks from Facebook, TheoryEngine::getExplanation was found to be the bottleneck, where the main loop of TheoryEngine::getExplanation would be run regularly 30k times, sometimes over 1 million times for a single conflict.
This caches explanations in this loop, where now the loop is executed roughly 1k times at max for the same benchmark.
One challenging benchmark that previously solved in 8 min 45 sec now solves in 2 min 45 sec.
FYI @barrettcw .
yoni206 [Sat, 11 Jul 2020 11:39:56 +0000 (04:39 -0700)]
Changing bv_to_int options (#4721)
This PR changes --solve-bv-as-int from a numerical option (specifying the granularity) to an enum (specifying the approach). Currently we support only two modes: OFF and SUM. Future PRs will add more modes.
The numerical value of the granularity is now captured by the new option --bvand-integer-granularity.
Tests are updated accordingly.
Haniel Barbosa [Sat, 11 Jul 2020 04:55:31 +0000 (01:55 -0300)]
Adding test for whether a kind is n-ary (#4718)
Andrew V. Jones [Sat, 11 Jul 2020 03:37:20 +0000 (04:37 +0100)]
Add support for printing 'get-abduct' in verbose mode (#4710)
Issue
For any of the following files:
test/regress/regress1/abduct-dt.smt2
test/regress/regress1/sygus-abduct-test-ccore.smt2
test/regress/regress1/sygus-abduct-test.smt2
test/regress/regress1/sygus-abduct-ex1-grammar.smt2
test/regress/regress1/sygus-abduct-test-user.smt2
test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
test/regress/regress1/sygus/abduction_streq.readable.smt2
test/regress/regress1/sygus/abd-simple-conj-4.smt2
test/regress/regress1/sygus/uf-abduct.smt2
test/regress/regress1/sygus/yoni-true-sol.smt2
running the following:
./bin/cvc4 -vvv <file>
would print:
Invoking: ERROR: don't know how to print a Command of class: N4CVC416GetAbductCommandE
Resolution
This PR adds support in src/printer/smt2/smt2_printer.cpp to be able to print a Command of type GetAbductCommand.
Given the similarities between get-abduct and synth-fun, I have refactored the printing logic in toStream(std::ostream& out, const SynthFunCommand* c) for a printing a SyGuS grammar to be shared between both SynthFunCommand and GetAbductCommand.
As a result, you now see something like this:
[avj@tempvm build]$ ./bin/cvc4 -vvv ../test/regress/regress1/abduct-dt.smt2
Invoking: (set-option :incremental false)
Invoking: (set-logic ALL)
Invoking: (declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
Invoking: (declare-fun x () List)
Invoking: (assert (distinct x nil))
minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy.
Invoking: (get-abduct A (= x (cons (head x) (tail x))))
(error "Cannot get abduct when produce-abducts options is off.")
Signed-off-by: Andrew V. Jones andrew.jones@vector.com