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
Andrew Reynolds [Sat, 11 Jul 2020 02:19:01 +0000 (21:19 -0500)]
(proof-new) Add ONCE and FIXPOINT modes for term conversion proof generator (#4709)
We need multiple policies for generic proofs for term conversion, in particular, substitution has a "apply once" semantics which does not apply rewrite steps to a fixpoint like the rewriter.
This is required for eliminating SUBS steps in the final proof.
Also note that an internal method for getting proofs was generalized, which will be required for doing multiple variants of proofs in this utility in the future.
Andrew Reynolds [Sat, 11 Jul 2020 00:03:24 +0000 (19:03 -0500)]
(proof-new) Update Theory interface for proof-new (#4648)
This includes 4 changes:
Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.
This PR is also contingent on the performance tests for proof-new on SMT-LIB.
Andres Noetzli [Fri, 10 Jul 2020 22:35:17 +0000 (15:35 -0700)]
Always Update Git information when rebuilding (#4696)
Commit
61734b41b7b96e7e7cbf46021a357d840d64b42e changed the way some of
our source files are generated. However, the change meant that once
`git_versioninfo.cpp` was generated, it was never updated again: The
custom command for `git_versioninfo.cpp` has no dependencies, so CMake
does not rebuild it unless the output file is missing [0]. This commit
reverts the change to our `gen-gitinfo` target and adds `git_versioninfo.cpp`
to `BYPRODUCTS` for the target to indicate that the file may have changed.
I am not sure if there is a better solution because we actually have to run
`GitInfo.cmake` to see if there have been any changes in the Git information.
Introducing a dependency on all source files is not sufficient because other
files or just the branch name may change. Note: The original solution only
updates the timestamp of `git_versioninfo.cpp` if its contents actually
change (`GitInfo.cmake` uses `configure_file()` to generate
`git_versioninfo.cpp`, which only updates the timestamp when the
contents changed [1]), so we don't do any unnecessary work.
[0] https://cmake.org/cmake/help/latest/command/add_custom_command.html
[1] https://cmake.org/cmake/help/latest/command/configure_file.html
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
Co-authored-by: Andrew V. Jones <andrew.jones@vector.com>
Andrew Reynolds [Fri, 10 Jul 2020 20:51:25 +0000 (15:51 -0500)]
Front end support for integer AND (#4717)
Ying Sheng [Fri, 10 Jul 2020 19:19:17 +0000 (12:19 -0700)]
[Interpolation] Add interface for SyGuS interpolation module (#4677)
This is the second step of adding Interpolation. 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 second step creates the component for computing interpolation, while omits the implementation.
Gereon Kremer [Fri, 10 Jul 2020 17:20:07 +0000 (19:20 +0200)]
Add deps/install/lib to RPATH and warn user when using dynamic libs. (#4684)
Installing the cvc4 binary does not work right now if it links against a shared library obtained via one of the contrib scripts.
This PR thus adds deps/install/lib to the RPATH so that the installed binary works at all in this case.
This change however paves the way to more problems: If one install such a dynamically linked binary and then removes (or updates) one the shared libraries in deps/install/lib, the installed binary most probably stops working.
Hence, this PR checks whether this may happen (whether we link dynamically and link against a shared library from deps/install/lib) and, if this is the case, informs and warns the user about this issue.
If the user tries to install to the default install prefix (/usr/local) we disallow installation entirely.
Andrew Reynolds [Fri, 10 Jul 2020 14:52:01 +0000 (09:52 -0500)]
Update competition scripts (#4715)
This PR creates a "current" sygus comp scripts, similar to what we have been doing for SMT COMP. It updates these scripts to fix the option names, as many have changed recently.
This also copies the SMT COMP current scripts to 2020, since they were used in the current state. @4tXJ7f let me know if this is not the case.
Andrew Reynolds [Fri, 10 Jul 2020 01:07:21 +0000 (20:07 -0500)]
Ensure legal elimination for witness rewrite (#4688)
Fixes #4685.
A recent commit #4661 added assertions for checking whether a witness rewrite corresponded to a legal elimination. #4685 demonstrates that these assertions can be violated and hence should be checked to ensure the rewrite is sound.
Andrew Reynolds [Thu, 9 Jul 2020 21:07:51 +0000 (16:07 -0500)]
Disable unsat cores in timeout regression (#4713)
Fixes a timeout in the nightlies.
One regression times out during unsat core checking. This appears to be random, the subcall to check for unsat-cores is applying sygus-inst in the expected way, however, it struggles to find the right instances.
Furthermore note that we are planning to redo implementation of unsat cores soon (when proof-new is fully merged), so we should revisit this (and all other) regressions with --no-check-unsat-cores when that happens.
Andrew Reynolds [Thu, 9 Jul 2020 20:21:08 +0000 (15:21 -0500)]
Associate all lemmas in non-linear arithmetic with an inference identifier (#4712)
This marks all lemmas in non-linear arithmetic with an identifier, which indicates informally the kind of justification that was used for them. The main motivation for this is for debugging the behavior of the non-linear solver.
The number of inferences can then be seen with --stats:
nl::inferences, [(SPLIT_ZERO : 19), (SIGN : 4), (COMPARISON : 29)]
The same design was used in strings and has been quite helpful.
This also adds a few high level stats to the new statistics class for non-linear.
Andrew Reynolds [Thu, 9 Jul 2020 05:41:47 +0000 (00:41 -0500)]
(proof-new) Theory engine proof generator (#4657)
This adds the proof generator used by TheoryEngine for generating proofs for explanations.
Gereon Kremer [Wed, 8 Jul 2020 21:24:24 +0000 (23:24 +0200)]
Re-implement handling of --tlimit (#4655)
As a first step within this project, this PR provides a new implementation that backs --tlimit. It uses setitimer (as timer_settime is not available on MacOS) to make the OS send a signal after the given wall clock time has passed.
In more detail, this PR:
removes the current handling of --tlimit (TlimitListener and its integration in the NodeManager)
adds a new TimeLimitListener that lives in src/main
uses TimeLimitListener directly in runCvc4()
adds a signal handler for SIGALRM (that also uses the existing timeout_handler)
Mathias Preiner [Wed, 8 Jul 2020 13:38:26 +0000 (06:38 -0700)]
Add getName() method to options. (#4704)
getName() returns the long option name if it exists and an empty string otherwise.
Andrew Reynolds [Wed, 8 Jul 2020 11:48:40 +0000 (06:48 -0500)]
Always interleave theory combination with quantifiers (#4703)
This removes an option setting that made quantifiers always run at full effort (before theory combination) when an undecidable theory was present. The intuition is that such theories may also be unfair wrt theory combination, so quantifiers might as well "join them" at full effort.
However, this option modification significantly hurts our performance in terms of timeouts on verification benchmarks from Facebook, where theory combination needs to run but quantifiers (alone) is preempting it from running. The correct solution is in fact to have other theories interleave with theory combination with the same policy as quantifiers (I've opened CVC4/cvc4-wishues#74).
Andrew Reynolds [Wed, 8 Jul 2020 00:50:01 +0000 (19:50 -0500)]
Improve and fix secant and tangent lemmas in the transcendental solver (#4689)
Fixes #4686.
This benchmark failed an assertion that corresponded to the fact that a refinement lemma did not evaluate to false in the current model (and hence does not rule out the current model).
This was caused by applying the rewriter in a way that led to an incorrect approximation. This meant that some tangent and secant lemmas would be ineffective.
The benchmark in that issue now times out, but makes progress in the refinement lemmas it generates.
This also simplifies and improves the use of approximated values (instead of model values) when constructing tangent and secant lemmas.
Andrew Reynolds [Tue, 7 Jul 2020 23:18:54 +0000 (18:18 -0500)]
Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)
This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.
The changes that were required for this PR include:
The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.
Andrew V. Jones [Tue, 7 Jul 2020 17:06:09 +0000 (18:06 +0100)]
Increase the minimum version of CMake due to the use of 'APPEND' with strings (#4702)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
Andrew Reynolds [Mon, 6 Jul 2020 23:48:10 +0000 (18:48 -0500)]
Front end support for sequences (#4690)
With this PR, we now support a preliminary draft of a theory of sequences.
This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them.
As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term.
We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++).
Andres Noetzli [Mon, 6 Jul 2020 23:06:55 +0000 (16:06 -0700)]
[GitHub] Add link to fuzzing guidelines in issues (#4695)
Andres Noetzli [Fri, 3 Jul 2020 00:14:22 +0000 (17:14 -0700)]
Remove SWIG bindings (#4683)
This commit removes support for SWIG bindings for the legacy API. The
bindings were already broken by
19054b3b1d427e662d30d4322df2b2f2361353da
and we are not planning on using SWIG for the Java API for the new API.
Andrew Reynolds [Thu, 2 Jul 2020 17:17:32 +0000 (12:17 -0500)]
Fix regression option (#4680)
Andrew Reynolds [Thu, 2 Jul 2020 13:33:49 +0000 (08:33 -0500)]
(proof-new) Updates to skolem manager interface (#4664)
Adds a fix for mkPurifySkolem and introduces new interfaces in preparation for arithmetic operator elimination and term formula removal proofs.
Andrew Reynolds [Thu, 2 Jul 2020 11:56:37 +0000 (06:56 -0500)]
(proof-new) Proof rule checkers run on skolem forms (#4660)
Previously, the proof rule checkers were run on witness form for convenience. However, it is more flexible for the sake of the internal calculus to run on Skolem forms. The main reason is that the conversion to/from witness form does not preserve terms that contain witness. Our preprocessing steps rely on using witness terms. This design change additionally simplifies a lot of the code of the builtin proof rule checker.
Instead, witness forms can be queried on an as-needed basis, e.g. in MACRO_SR_PRED_TRANSFORM.
Andrew Reynolds [Thu, 2 Jul 2020 10:48:09 +0000 (05:48 -0500)]
(proof-new) Proof node updater (#4647)
Adds utility for updating proof nodes. The module for post-processing proof nodes in the SmtEngine for the sake of proof conversion to external formats will build on this utility.
Requires #4617.
Andrew Reynolds [Wed, 1 Jul 2020 19:54:41 +0000 (14:54 -0500)]
Add solver for integer AND (#4681)
This omits certain inference schemas (sum and bitwise lemmas) which depends on an option that will be added later.
Andres Noetzli [Wed, 1 Jul 2020 15:44:21 +0000 (08:44 -0700)]
Add testing infrastructure for LFSC signatures (#4678)
This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts run_test.py from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from proofs/signatures as the initial
set of tests.
Co-authored-by: Alex Ozdemir aozdemir@hmc.edu
Andrew Reynolds [Wed, 1 Jul 2020 13:46:07 +0000 (08:46 -0500)]
Inferences and model construction taking into account seq.unit (#4607)
Towards theory of sequences.
This makes the strings solver handle seq.unit, which requires two new inferences and updates to its model construction.
It also fixes a bug in the best content heuristic, which previously failed to update the best score.
Andrew Reynolds [Wed, 1 Jul 2020 06:10:09 +0000 (01:10 -0500)]
(proof-new) Updates to evaluator (#4659)
This will be required to separate "evaluation steps" from "rewrite steps" when reconstructing proofs of rewrites.
Andrew Reynolds [Wed, 1 Jul 2020 04:48:08 +0000 (23:48 -0500)]
(proof-new) Improve rewriter for WITNESS (#4661)
Proof checking failures revealed that we are not rewriting witness for Boolean variables (witness ((x Bool)) x) ---> true and (witness ((x Bool)) (not x)) ---> false.
Also adds 2 assertions that are required for elimination (witness ((x T)) (= x t)) ---> t. These assertions should always hold due to the witness terms we construct.
Andrew Reynolds [Tue, 30 Jun 2020 23:08:54 +0000 (18:08 -0500)]
Fix normal form for re.comp (#4676)
Fixes #4674.
Andres Noetzli [Tue, 30 Jun 2020 21:53:46 +0000 (14:53 -0700)]
Update NEWS post 1.8 release (#4666)
Mathias Preiner [Tue, 30 Jun 2020 19:12:25 +0000 (12:12 -0700)]
Fix GMP compilation for win64. (#4675)
Andrew Reynolds [Tue, 30 Jun 2020 16:12:39 +0000 (11:12 -0500)]
Simplify quantifiers strategy for when to apply last call effort check with fmfBound (#4673)
There was a strategy in place for alternating which rounds quantifier instantiation would run on when --fmf-bound is enabled.
However, this made it so that in some cases, no instantiation strategy would be applied, if e.g. fmfBound was enabled but no quantified formulas were handled by that strategy.
It is not clear if this strategy is a good idea, considering all use cases of quantifiers, and hence this PR deletes this block of code.
This makes it so that several eqrange benchmarks are answered "unsat" quickly.
Ying Sheng [Tue, 30 Jun 2020 11:50:40 +0000 (04:50 -0700)]
Interpolation step 1 (#4638)
This is the first step of adding Interpolation. 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 first step creates the API framework, while omits the implementation for getting interpolation.
Mathias Preiner [Tue, 30 Jun 2020 07:24:07 +0000 (00:24 -0700)]
contrib: Update to GMP 6.2.0, compile static and shared libraries. (#4671)
Andrew Reynolds [Tue, 30 Jun 2020 02:55:51 +0000 (21:55 -0500)]
Add internal support for integer and operator (#4668)
Towards merging iand branch to master. This adds internal support for an "integer AND" operator.
Andres Noetzli [Mon, 29 Jun 2020 22:35:44 +0000 (15:35 -0700)]
Make ExprManager constructor private (#4669)
This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.
makaimann [Mon, 29 Jun 2020 21:28:17 +0000 (14:28 -0700)]
Python Sort tests (#4639)
This commit ports over the sort_black tests to the pytest infrastructure to test the Python bindings. It also adds missing functionality that was revealed during the testing.
Andres Noetzli [Mon, 29 Jun 2020 20:01:09 +0000 (13:01 -0700)]
Fix memory leak in unit test node_algorithm_black (#4670)
Commit
ccd4500 modified the unit test
node_algorithm_black. It added d_bvTypeNode as a data member to the
class and initialized it in setUp() but did not free it in
tearDown(), which set off ASan. This commit fixes tearDown() to free
d_bvTypeNode.
Marking this as major because it should fix the nightlies.
Andrew Reynolds [Sun, 28 Jun 2020 13:34:44 +0000 (08:34 -0500)]
Fix non-termination issues in simpleRegExpConsume (#4667)
There were two issues related to RE in bodies of re.* that accepted the empty string that led to non-termination in the rewriter for regular expressions.
This also improves trace messages for simpleRegExpConsume.
Fixes #4662.
Alex Ozdemir [Sun, 28 Jun 2020 12:51:31 +0000 (05:51 -0700)]
Proof Rules and Checker for Arithmetic (#4665)
This PR introduces proof rules for arithmetic and their checker.
The code is dead, since these rules are never used.
Andres Noetzli [Sat, 27 Jun 2020 07:12:26 +0000 (00:12 -0700)]
Add API for retrieving separation heap/nil term (#4663)
This commit extends the API to support the retrieval of heap/nil term
when separation logic is used and changes the corresponding system test
accordingly. This commit is in preparation of making the constructor of
`ExprManager` private.
yoni206 [Fri, 26 Jun 2020 02:36:59 +0000 (19:36 -0700)]
fix and test (#4658)
This PR adds support for indexed operators (such as extract) to getOperatorsMap in node_algorithm.cpp. The corresponding test is augmented accordingly.