Haniel Barbosa [Tue, 29 Sep 2020 12:35:46 +0000 (09:35 -0300)]
[proof-new] Adds a proof-producing CNF converter (#5137)
A proof generator that wraps the original CNF stream, to be used when the prop engine is proof producing. It tracks in a lazy cdproof both the concrete clausification steps and the proof generators of the formulas being clausified (in particular, theory lemmas).
Gereon Kremer [Tue, 29 Sep 2020 12:05:46 +0000 (14:05 +0200)]
Clean up nonlinear extension (#5149)
This PR performs some cleanups in the nonlinear extension, in particular it removes the old lemma collection scheme. It is no longer needed, as all subsolvers use the inference manager.
Andrew Reynolds [Tue, 29 Sep 2020 03:56:20 +0000 (22:56 -0500)]
Reset assertions on resetAssertions (#5153)
The assertions object is currently not cleared on resetAssertions, only the prop engine is reset. This means that if a user added assertion, did not use them in a check-sat, and then called reset-assertions, they would not be removed from the assertions pipeline (storing the pending assertions before they are sent to the prop engine).
This fixes #5144.
Alex Ozdemir [Tue, 29 Sep 2020 03:14:47 +0000 (20:14 -0700)]
Add utilities for arith/proof_checker and build it (#5157)
The arith proof checker was not being built (not in cmake). Now it is. A
few dependencies were missing.
Haniel Barbosa [Tue, 29 Sep 2020 02:34:34 +0000 (23:34 -0300)]
[proof-new] Removing spurious forward declaration in CnfStream (#5155)
Haniel Barbosa [Tue, 29 Sep 2020 01:22:29 +0000 (22:22 -0300)]
[proof-new] Adds a proof node hash function (#5154)
Andrew Reynolds [Tue, 29 Sep 2020 00:54:25 +0000 (19:54 -0500)]
Disable regression that is timing out (#5142)
Seems to be timing out on 1/5 of our CI runs currently.
Andrew Reynolds [Mon, 28 Sep 2020 23:33:03 +0000 (18:33 -0500)]
Minor fixes to quantifiers proofs (#5151)
Includes minor changes to the proof checker and a fix in the instantiate module.
Haniel Barbosa [Mon, 28 Sep 2020 20:38:59 +0000 (17:38 -0300)]
[proof-new] Adds a proof manager for the SAT solver (#5140)
Tracks the refutation proof built by Minisat. See the header for extensive explanations.
This commit also adds a few dependencies for the SAT proof manager to work (making it a friend of the SAT solver, getting the cnf stream from theory proxy, having lazy cdproof chain give all the links).
mudathirmahgoub [Mon, 28 Sep 2020 13:53:07 +0000 (08:53 -0500)]
Implement bags rewriter (#5132)
This PR implements rewrite rules for bags. This PR focuses on rewrite rules for non constant nodes.
Rewriting nodes with constant children is delegated to bags::NormalForm class (future PR).
Gereon Kremer [Mon, 28 Sep 2020 11:48:26 +0000 (13:48 +0200)]
Add new arithmetic BoundInference class (#5148)
This PR adds a new utility class that extracts bounds on single variables from theory atoms like x > 0 or y <= 17. It does not perform further reasoning (like recognizing x > y with y > 3 as a bound).
Note that the functionality was introduced in arith/nl/icp/variable_bounds.h, but is now available using Node only.
This PR also replaces the VariableBounds by BoundInference in the icp solver which allowed for checking the code.
Andrew Reynolds [Sun, 27 Sep 2020 22:29:02 +0000 (17:29 -0500)]
Fix sygus quantifier elimination preprocess for multiple functions (#5130)
The option --sygus-qe-preproc performs quantifier elimination to coerce certain synthesis conjectures to be single invocation. This technique was broken when multiple synthesis functions were present. This fixes the issue and adds a regression where --sygus-qe-preproc enables a benchmark to be quickly solved.
Gereon Kremer [Sat, 26 Sep 2020 17:11:13 +0000 (19:11 +0200)]
Use inference manager for nl_solver (#5125)
This PR migrates the nl_solver part of the nonlinear extension to use the new inference manager as well.
It adds a new method clearWaitingLemmas to the inference manager and uses ArithLemma (though NlLemma exists) as we don't need the additional functionality of NlLemma.
Andrew Reynolds [Sat, 26 Sep 2020 15:07:42 +0000 (10:07 -0500)]
Connect the shared solver to theory engine (#5103)
This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database.
It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus.
This PR has no intended behavior changes.
FYI @barrettcw
Andrew Reynolds [Sat, 26 Sep 2020 13:51:57 +0000 (08:51 -0500)]
Use original quantified formula for single invocation reconstruction (#5129)
This fixes an issue with single invocation solution reconstruction where the preprocessed quantified formula contains internal skolems, thus prohibiting reconstruction. The solution is to use the original quantified formula when doing solution reconstruction. This adds a regression demonstrating the issue.
Aina Niemetz [Sat, 26 Sep 2020 01:08:08 +0000 (18:08 -0700)]
Restrict bvxnor to only allow two operands (was n-ary). (#5138)
Bit-vector operator bvxnor was previously mistakenly marked as
left-assoicative in SMT-LIB. This has recently been corrected in
SMT-LIB. We now restrict bvxnor to only allow two operands in order to
avoid confusion about the semantics, since the behavior of n-ary
operands to bvxnor is now undefined in SMT-LIB.
Andrew Reynolds [Fri, 25 Sep 2020 18:45:38 +0000 (13:45 -0500)]
Make sygus refinement step more robust to unevaluatable counterexamples (#5102)
Currently, the CEGIS refinement loop of the sygus solver may terminate with "unknown" when a duplicate counterexample is generated. This is caused by a candidate t for a conjecture exists f. forall x. G[f, x] such that:
(1) G[t, c] evaluates to a non-constant expression,
(2) ~G[t, k] is satisfiable with model k = c.
Notice this exclusively limited to theories with incomplete functions, e.g. (non-linear) division.
In this case, we know that t is an incorrect solution, but the counterexample we found was not new.
Currently, we abort with "unknown" since the counterexample was not new. After this PR, we exclude t and continue, which is uncontroversially the correct behavior.
This PR moves the resposibility for lemma from synth engine to synth conjecture, which simplifies the behavior of the main check conjecture method.
Haniel Barbosa [Fri, 25 Sep 2020 15:24:06 +0000 (12:24 -0300)]
Cleaning and documenting cnf stream (#5134)
Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.
Aina Niemetz [Thu, 24 Sep 2020 22:47:41 +0000 (15:47 -0700)]
SyGuS: Add default grammar for FP. (#5133)
Andrew Reynolds [Thu, 24 Sep 2020 20:02:04 +0000 (15:02 -0500)]
Function definition fmf preprocessing pass (#5064)
This defines the function definition finite model finding as a proper preprocessing pass.
This is required for cleaning/fixing bugs in the preprocessor on proof-new.
There are no intended behavior changes in this PR, although the code for the pass was updated to the new style guidelines.
Andrew Reynolds [Thu, 24 Sep 2020 03:13:35 +0000 (22:13 -0500)]
Modify lemma vs fact policy for datatype equalities (#5115)
This changes the lemma vs fact policy for datatype equalities. Previously, datatype equalities were sent as lemmas unless they were over datatypes that were composed of datatypes only. This is now changed so that equalities that do not involve direct subterms with finite non-datatype types are kept internal.
The primary type of equality that this targets are "Instantiate" equalities, e.g. the conclusion of:
(is-cons x) => x = (cons (head x) (tail x))
These equalities have been observed to generate large amounts of new terms for many benchmarks.
With this PR, the the challenging Facebook benchmark goes from 2 min 45 sec -> 29 sec. If the instantiate rule is disabled altogether, it still correctly solves, and is faster (~14 seconds), which however is not correct in general.
This change triggered two other issues:
(1) A relations benchmark involving transitive closure now times out. This has been a common issue for the relations solver and should be revisited.
(2) A potential issue with doPendingLemmas in InferenceManagerBuffer was uncovered. In rare cases, we can be re-entrant into this method since OutputChannel::lemma may trigger further preregistration of terms, which can trigger a recursive call to doPendingLemmas in the case of datatypes, which causes a segfault due to corrupting an iterator. This PR adds a simple guard for this method.
This PR also fixes some existing issues in computing cardinality for parametric datatypes.
Andrew Reynolds [Wed, 23 Sep 2020 19:56:52 +0000 (14:56 -0500)]
Disable cegqi-bv when using sygus (#5124)
This disables the CAV 2018 techniques for BV quantifier instantiation when solving sygus since they may generate terms with witness in them. This adds a regression where this occurs.
I've opened an cvc4 projects issue to revisit this (CVC4/cvc4-projects#227).
Gereon Kremer [Wed, 23 Sep 2020 18:05:06 +0000 (20:05 +0200)]
Make IAND solver use inference manager. (#5126)
This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas.
Aina Niemetz [Wed, 23 Sep 2020 16:15:39 +0000 (09:15 -0700)]
Missing format from #5112.
yoni206 [Wed, 23 Sep 2020 13:00:59 +0000 (06:00 -0700)]
bv2int: new options for bvand translation (#5096)
Currently, (bvand x y) is translated into a sum of ITEs.
This PR introduces two more options for the translation of (bvand x y):
bv: cast the integer translations of x and y back to bit-vectors, do a bvand, and cast the result to integers.
iand: use the builtin iand operator.
These options are added to many of the tests, and some new tests are added.
In addition, some tests are cleaned up (e.g., removing --no-check-unsat-cores for satisfiable benchmarks).
Finally, some tests are moved from regress0 to regress2 because they take several seconds to complete (2 -- 10 seconds).
Andrew Reynolds [Wed, 23 Sep 2020 04:50:43 +0000 (23:50 -0500)]
Allow E-matching by default when strings are enabled (#5117)
This does not disable E-matching when strings are enabled with --strings-exp, due to potential applications where strings are combined with user-provided quantified formulas.
Notice that by default, we do not want E-matching applied to quantified formulas corresponding to reductions for extended string functions. To correct this, all quantified formulas generated by strings are marked with an "internal quantified formula" attribute, which causes E-matching to ignore them. This feature can in theory be generalized later for other internal sources of quantified formulas.
Aina Niemetz [Wed, 23 Sep 2020 04:25:07 +0000 (21:25 -0700)]
New C++ API: Catch and throw recoverable exception. (#5122)
This allows to distinguish recoverable from non-recoverable exceptions,
and recover if possible.
Aina Niemetz [Wed, 23 Sep 2020 03:46:17 +0000 (20:46 -0700)]
FP: Use Assert instead of AlwaysAssert in traits::(pre|post)condition. (#5121)
For the same reason as in #5119.
Abdalrhman Mohamed [Wed, 23 Sep 2020 03:12:17 +0000 (22:12 -0500)]
Refactor Commands to use the Public API. (#5105)
This is work towards eliminating the Expr layer. This PR does the following:
Replace Expr/Type with Term/Sort in the API for commands.
Remove the command export functionality which is not supported.
Since many commands now call the Solver functions instead of the SmtEngine ones, their behavior may be a slightly different. For example, (get-unsat-assumptions) now only works in incremental mode. In some cases, CVC4 will not recover from non-fatal errors.
Andrew Reynolds [Wed, 23 Sep 2020 01:06:42 +0000 (20:06 -0500)]
Fix type issue with term formula removal (#5107)
We currently are using lookups with uint32_t but storing with int32_t. Somehow the compilers don't complain, but I noticed this was mismatched.
Andres Noetzli [Wed, 23 Sep 2020 00:41:09 +0000 (17:41 -0700)]
[Python API] Conversion to/from Unicode strings (#5120)
Fixes #5024. This commit adds a conversion from constant string terms to
native Python Unicode strings in Term.toPythonObj() and improves
Solver.mkString() to accept strings containing characters outside of
the printable range.
Aina Niemetz [Tue, 22 Sep 2020 23:15:54 +0000 (16:15 -0700)]
FP: Use Assert instead of PRECONDITION macro in converter. (#5119)
The FP converter (= word blaster) uses a PRECONDITION macro that is
defined in symFPU (if included) and calls traits::precondition. This is
a problem for two reasons. First, traits::precondition calls
AlwaysAssert, and PRECONDITION is called for every word-blasted node, so
this can be expensive. Second, in case of an assertion failure, we get
very generic failure messages, that don't allow to distinguish between
failures and are absolutely non-descriptive:
Check failure
b
This fixes both issues.
@martin-cs
Mathias Preiner [Tue, 22 Sep 2020 22:40:48 +0000 (15:40 -0700)]
Add simple BV solver (#5065)
This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.
mudathirmahgoub [Tue, 22 Sep 2020 21:59:41 +0000 (16:59 -0500)]
Add skeleton for theory of bags (multisets) (#5100)
This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.
Andres Noetzli [Tue, 22 Sep 2020 19:13:33 +0000 (12:13 -0700)]
Fix compilation without LibPoly (#5118)
Commit
e969318 introduced the ICP-based
solver for nonlinear arithmetic. That code, however, depends on LibPoly.
When configuring CVC4 without LibPoly, the code doesn't compile because
the class ICPSolver is missing. This commit adds a dummy version if
ICPSolver to remedy the issue.
makaimann [Tue, 22 Sep 2020 18:58:03 +0000 (11:58 -0700)]
Add method to get Python object from constant value term in Python API (#5083)
This PR addresses issue https://github.com/CVC4/CVC4/issues/5014. It simply interprets the SMT-LIB string representation and produces a Python object. It currently supports booleans, ints, reals, bit-vectors, and arrays. The method (`toPythonObj`) is only valid to call if `isConst` returns true.
Mathias Preiner [Tue, 22 Sep 2020 16:51:56 +0000 (09:51 -0700)]
Update copyright header script to support CMake and Python files (#5067)
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
Gereon Kremer [Tue, 22 Sep 2020 15:49:46 +0000 (17:49 +0200)]
ICP-based solver for nonlinear arithmetic (#5017)
This PR adds a new icp-based solver to be integrated into the nonlinear extension.
It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence.
yoni206 [Tue, 22 Sep 2020 01:44:26 +0000 (18:44 -0700)]
Require dumping in a dumping test (#5108)
Add ; REQUIRES: dumping to a dumping test.
Fixes nightlies.
Andrew Reynolds [Mon, 21 Sep 2020 17:09:33 +0000 (12:09 -0500)]
(proof-new) Add the arrays proof checker (#5047)
Includes adding the standard method for constructing the extensionality skolem using the skolem manager.
Andrew Reynolds [Sun, 20 Sep 2020 15:59:36 +0000 (10:59 -0500)]
More flexible design for model manager distributed (#4976)
This PR makes it so that the distributed model manager can be used independently of the architecture for equality engine management for theories, meaning the choice of using a separate equality engine for the model can be done in both the current distributed architecture, or the proposed central architecture (where there would be 2 equality engines, the central one and the model one). The "central model manager" on the other hand will only be combined with the central architecture. This will make it easier to test the centralized equality engine manager, since all things related to model construction can be preserved when using a central architecture.
This PR moves some of the responsibilities from the (distributed) equality engine manager to the distributed model manager, including the management of the context of the model equality engine and the allocation of its equality engine.
This PR is not intended to make any behavior changes to the current architecture.
Andrew Reynolds [Sat, 19 Sep 2020 15:57:51 +0000 (10:57 -0500)]
Standardize equality engine notifications in sets (#5098)
Andrew Reynolds [Fri, 18 Sep 2020 20:49:40 +0000 (15:49 -0500)]
Fix assertion list for globally defined recursive functions (#5084)
This was uncovered by a (spurious) proof checking failure on proof-new.
Andrew Reynolds [Fri, 18 Sep 2020 17:52:16 +0000 (12:52 -0500)]
Add the shared solver (#4982)
This PR adds the definition for the "shared solver", it does not connect it to TheoryEngine/CombinationEngine yet. This is an object that behaves like a "glue" theory solver and has a special role in TheoryEngine.
In the current architecture, the "SharedTermsDatabase" is the "shared solver", although in the central architecture, the shared solver will be required to behave differently. This PR adds the abstract definition of shared solver, where notice SharedSolverDistributed is a thin layer on top of SharedTermsDatabase.
In a followup PR, CombinationEngine will maintain a shared solver and ~5 blocks of code in TheoryEngine will be callbacks to the SharedSolver. Also, eventually the code for SharedTermsDatabase should be split: the parts involving equality reason/propagation/explanation should be migrated into SharedSolverDistributed, and the parts related to registration will remain in SharedTermsDatabase (to also be used in the planned SharedSolverCentral).
FYI @barrettcw
yoni206 [Fri, 18 Sep 2020 17:12:04 +0000 (10:12 -0700)]
bv2int: quantifiers support (#5080)
This PR adds quantifiers support for bv2int preprocessing pass, and adds regressions that use quantifiers.
Andres Noetzli [Fri, 18 Sep 2020 16:53:23 +0000 (09:53 -0700)]
Fix muzzled builds (#5093)
Commit
2c2f05c moved some function
definitions from dump.h to dump.cpp, which is good. However, the
corresponding definitions for muzzled builds weren't moved, so muzzled builds
defined the operator << multiple times. This made our nightly
competition build fail. This commit fixes the issue by moving the
alternative definitions to the source file as well.
Haniel Barbosa [Fri, 18 Sep 2020 16:32:47 +0000 (13:32 -0300)]
[proof-new] Proof utilities for normalizing clauses at the Node level (#5089)
Extends Theory Proof Step Buffer. These utilities are used so that we can account for the fact that Minisat silenly does these transformations on added clauses.
Andrew Reynolds [Fri, 18 Sep 2020 15:07:12 +0000 (10:07 -0500)]
Logic exception for arrays indexed by arrays (#5073)
This throws a logic exception when a term of array type whose index is also an array is registered to the theory of arrays.
It refactors the preRegisterTermInternal method of arrays so that all non-equality terms are added to the equality engine in the same block of code, which also checks for the type.
Fixes #4237.
FYI @barrettcw
Andres Noetzli [Fri, 18 Sep 2020 14:40:26 +0000 (07:40 -0700)]
[Strings] Fix extended equality rewriter (#5092)
Fixes #5090. Our extended equality rewriter was performing the following
unsound rewrite:
(= (str.++ Str13 Str5 Str16 Str13) (str.++ Str5 Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")) ---> (and (= (str.++ Str13 Str5) Str5) (= (str.++ Str16 Str13) (str.++ Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")))
The rule being applied was SPLIT_EQ_STRIP_R. The rewrite was applied
due to the following circumstances:
The rewriter found that (str.++ Str13 Str5) is strictly shorter than (str.++ Str5 Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")
The rewriter stripped the symbolic length of the former from the
latter
stripSymbolicLength() was only able to strip the first component, so
there was a remaining length of (str.len Str13)
The rule SPLIT_EQ_STRIP_R, however, was implicitly assuming that the
symbolic length can either be stripped completly or not at all and was
not considering the case where only a part of the length can be
stripped.
The commit adds a flag to stripSymbolicLength() that makes the
function only return true if the whole length can be stripped from the
input. The commit also refactors the code in stripSymbolicLength()
slightly.
Note: It is not necessary to try to do something smart in the case where
only a partial prefix can be stripped because the rewriter tries to
apply the rule to all the different prefix combinations anyway.
Andrew Reynolds [Fri, 18 Sep 2020 02:38:42 +0000 (21:38 -0500)]
(proof-new) Updates to proof node updater algorithm (#5088)
This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating.
This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update.
Andrew Reynolds [Fri, 18 Sep 2020 02:06:44 +0000 (21:06 -0500)]
(proof-new) Rewrites involving operators in term conversion proof generator (#5072)
In some cases, e.g. witness form conversion, we require traversing to operators in term conversion proofs. This updates the term conversion generator to support (term-context-sensitive) rewrites involving operators using HO_CONG. This requires updating the term context utilities with support for operators.
Andrew Reynolds [Thu, 17 Sep 2020 21:57:05 +0000 (16:57 -0500)]
(proof-new) Fixes for theory engine proof generator (#5087)
Fixes an issue where conflicts stored in the theory engine proof generator where expecting to be (=> F false) instead of (not F).
Haniel Barbosa [Thu, 17 Sep 2020 21:22:21 +0000 (18:22 -0300)]
[proof-new] Have mkScope agnostic to True assumptions (#5086)
Gereon Kremer [Thu, 17 Sep 2020 20:44:53 +0000 (22:44 +0200)]
(cad-solver) Fix square-free-basis computation (#5085)
This PR fixes a subtle issue when making the polynomials of two subsequent (overlapping) intervals relative square-free. We now make sure that the resulting polynomials are ignored (if constant) or pushed to the lower dimension (if lower main variable). Also, we now appropriately update the main polynomials of the corresponding intervals.
Andrew Reynolds [Thu, 17 Sep 2020 19:43:24 +0000 (14:43 -0500)]
Reduce recursion in term formula removal (#5052)
This reduces the use of recursion in term formula removal module. The recursion depth is now limited to the number of term positions on a path where a formula must be removed, instead of being limited to the overall formula depth. This PR also fixes some documentation.
Notice for its main cache d_tfCache, this class uses a CDInsertHashMap (instead of a CDHashMap) which does not allow inserting more than once, hence an auxliary "processedChildren" vector had to be introduced to track whether we have processed children. It's not clear to me whether we should just use the more standard CDHashMap, which would simplify this.
One non-linear arithmetic regression went unsat -> unknown, I added --nl-ext-tplanes to fix this.
This should fix #4889. It is possible to further reduce the recursion in this pass, which can be done on a followup PR if needed.
Gereon Kremer [Thu, 17 Sep 2020 13:54:02 +0000 (15:54 +0200)]
Use new inference manager in transcendental solver (#5022)
This refactors the transcendental solver to add lemmas to the new inference manager instead of using the old lemma collection scheme.
Andrew V. Jones [Thu, 17 Sep 2020 07:18:43 +0000 (08:18 +0100)]
Do not allow to build Python bindings if building statically (#4784)
This PR disables building the Python bindings if you're doing a static build (which makes sense, because there's no such thing as a "static" Python module).
Signed-off-by: Andrew V. Jones andrew.jones@vector.com
Andrew Reynolds [Thu, 17 Sep 2020 05:22:20 +0000 (00:22 -0500)]
Further standardization of datatypes (#5076)
We now have no custom calls to equality engine explain, and only 2 manual calls to equality engine (in its entailment check). This also updates the notify class to the standard one.
This commit makes datatypes ready to start work on proofs.
yoni206 [Thu, 17 Sep 2020 03:34:40 +0000 (20:34 -0700)]
Dumping internal define-funs with no arguments (#5077)
Currently, --dump=assertions:... fails if a define-fun command is executed internally (an example for this can be found here.
The failure occurs because the printer expects a range type whenever a define-fun command is executed. However, when this command is used for 0-ary functions (variables), the getter for the range fails.
This PR fixes this by asking for a range only if the type is indeed a function. Otherwise, the original type is printed.
A test that currently fails but passes with this PR is included.
Andres Noetzli [Wed, 16 Sep 2020 20:36:05 +0000 (13:36 -0700)]
Only rewrite replace_re(_all) if regexp is const (#5075)
Fixes #5074. This commit fixes an issue in the rewriter of
str.replace_re and str.replace_re_all. For both operators, we do two
kinds of rewrites: (1) If the first argument is a constant, then we
check whether the regular expression appears in that constant and (2) we
check whether the regular expression matches the empty string. Both of
those checks were assuming a constant regular expression but there was
no guard in place for it. This commit adds the missing guard.
Abdalrhman Mohamed [Wed, 16 Sep 2020 17:45:01 +0000 (12:45 -0500)]
Dump commands in internal code using command printing functions. (#5040)
This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
Andrew Reynolds [Wed, 16 Sep 2020 16:57:59 +0000 (11:57 -0500)]
Add buffered inference manager to TheorySep (#5038)
This makes TheorySep use a standard buffered inference manager. Notice the behavior in TheorySep::doPending was simplified to assert both facts and lemmas. Previously, this was doing something strange: if there were any lemmas, then both facts and lemmas would be processed as lemmas, otherwise the facts would be processed as facts. Notice that TheorySep currently does not use facts by default. This design can be addressed in the future.
Note this PR eliminates the need for a custom explain method in TheorySep.
Haniel Barbosa [Wed, 16 Sep 2020 16:25:33 +0000 (13:25 -0300)]
[proof-new] Adds Lazy CDProof chain data-structure (#5060)
A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.
Andrew Reynolds [Wed, 16 Sep 2020 15:21:40 +0000 (10:21 -0500)]
Refactor collectModelInfo in TheoryArith (#5027)
This is work towards updating the arithmetic solver to the new standard, and in particular isolating TheoryArithPrivate as the "linear solver", and TheoryArith as the overall approach for arithmetic.
This transfers ownership of the non-linear extension from TheoryArithPrivate to TheoryArith. The former still has a pointer to the non-linear extension, which will be removed with further refactoring.
This PR additionally moves the code that handles the interplay of the non-linear extension in TheoryArithPrivate::collectModelInfo to TheoryArith, and simplifies the model interface for TheoryArithPrivate.
yoni206 [Wed, 16 Sep 2020 04:31:10 +0000 (21:31 -0700)]
bv2int: support models in tests (#5068)
Previous changes in this preprocessing pass have already enabled model generation when using it.
However, the satisfiable tests still had --no-check-models.
The changes in this PR:
All --no-check-models from current tests for the preprocessing pass are removed.
Refactoring of the relevant part of the code.
Solves CVC4/cvc4-projects#128.
Remark: disabling white-spaces when reviewing this PR is recommended.
Haniel Barbosa [Wed, 16 Sep 2020 03:30:49 +0000 (00:30 -0300)]
[proof-new] Extending eqproof conversion to HO congruence (#5071)
Haniel Barbosa [Wed, 16 Sep 2020 03:05:10 +0000 (00:05 -0300)]
[proof-new] Resolution rules and checkers (#5070)
Haniel Barbosa [Wed, 16 Sep 2020 02:36:21 +0000 (23:36 -0300)]
[proof-new] A simple proof generator for buffered proof steps (#5069)
This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Andrew Reynolds [Wed, 16 Sep 2020 01:47:43 +0000 (20:47 -0500)]
(proof-new) Make proofs mandatory in proof equality engine (#5059)
All uses of proof equality engine are now guarded such that the ordinary equality engine is used when proofs are not enabled. Thus, we can make proofs mandatory in proof equality engine. This eliminates the need for some guards.
Some indentation changed, but there are no additions in this PR.
Andrew Reynolds [Tue, 15 Sep 2020 16:07:21 +0000 (11:07 -0500)]
Move sets member propagation to SolverState (#5045)
This eliminates the parent relationship from solver state to theory sets.
Aina Niemetz [Tue, 15 Sep 2020 04:21:03 +0000 (21:21 -0700)]
Rename system tests to api tests and remove obsolete Java test. (#5066)
Andrew Reynolds [Tue, 15 Sep 2020 03:13:38 +0000 (22:13 -0500)]
Move quantifiers engine private to own file (#5053)
This moves and renames the quantifiers engine private class to QuantifiersModules. This is in preparation for using a standard state and inference manager object in TheoryQuantifiers and QuantifiersEngine.
Initializing quantifiers engine is a bit non-standard since it is intentionally a separate entity from TheoryQuantifiers. However, the plan is for quantifiers engine to use the state and inference manager of TheoryQuantifiers.
This PR additionally moves the initialization of quantifiers modules to a QuantifiersEngine::finishInit() method. The motivation for is that we do not have a state and inference manager during construction of QuantifiersEngine, since these will live in TheoryQuantifiers and will be passed to QuantifiersEngine during TheoryQuantifiers::finishInit. This means that we need a final pass to initialize quantifiers engine after these are initialized, which thus must come as the last step of TheoryEngine::finishInit.
The next PR will connect the state and inference manager to QuantifiersEngine during TheoryQuantifiers::finishInit. Then, the plan is for many of the core utilities in QuantifiersEngine to migrate to state/inference manager, and finally for its modules to reference state and inference manager instead of QuantifiersEngine.
Andrew Reynolds [Tue, 15 Sep 2020 02:58:08 +0000 (21:58 -0500)]
Fix needsModel method for CEGQI (#5048)
There was a bug in CEGQI's needModel method which could say that it doesnt need a model built when there are no active quantifiers. However, computing active quantifiers is not done in QuantifiersEngine::check until after this method is called, meaning it was using stale data on whether a quantifier was active or not. This could lead to the use of bogus models in CEGQI in incremental mode in some corner cases, leading to the assertion failure in #5019.
Fixes #5019.
Andrew Reynolds [Tue, 15 Sep 2020 02:19:15 +0000 (21:19 -0500)]
Standard equality engine notify class for Theory (#5042)
This makes a standard equality engine notify class that forwards the 3 mandatory callbacks to the provided inference manager (the other 3 callbacks may be specific to the theory). It updates TheoryUF to use this class, other theories will be updated to this style as more inference manager are added.
Notice that we could also forward the other 3 callbacks in this class to Theory, making eqNotifyNewClass, eqNotifyMerge, and eqNotifyDisequal virtual methods in Theory, which can be done on a future PR if needed.
Andres Noetzli [Tue, 15 Sep 2020 02:09:03 +0000 (19:09 -0700)]
Fix ABC build (#5061)
For some reason, our ABC build was including cnf_stream.h in an
extern "C" block instead of outside of it, which made the build fail
because the header indirectly includes cdqueue.h, which uses
templates. This change is older
(
e9bfbb2)
but only started causing problems with our nightly builds recently.
Ying Sheng [Tue, 15 Sep 2020 01:47:15 +0000 (09:47 +0800)]
Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)
Add interface for SyGuS Interpolation module. 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.
yoni206 [Mon, 14 Sep 2020 21:46:51 +0000 (14:46 -0700)]
bv2int: simpler translation for plus and times (#5055)
This PR makes the translation of plus and times by:
using plain mod rather than introducing a skolem. If this proves to be a bottleneck, we can try to tackle it where mod is treated in the solver in the future. This will make it easier to introduce support for quantifiers, as we don't need to introduce new variables under quantification.
Making sure everything is binarized in more places of the translation.
Andrew Reynolds [Mon, 14 Sep 2020 17:49:58 +0000 (12:49 -0500)]
Refactoring the rewriter of sets (#4856)
Changes it so that we don't flatten unions if at least one child is non-constant, since this may lead to children that are non-constant by mixing constant/non-constant elements and is generally expensive for large unions of singleton elements.
The previous rewriting policy was causing an incorrect model in a separation logic benchmark reported by Andrew Jones, due to unions of constant elements that were unsorted (and hence not considered constants). We now have the invariant that all subterms that are unions of constant elements are set constants.
Note this PR changes the normal form of set constants to be (union (singleton c1) ... (union (singleton cn-1) (singleton cn) ... ) not (union ... (union (singleton c1) (singleton c2)) ... (singleton cn)).
It changes a unit test which was impacted by this change which was failing due to hardcoding the enumeration order in the unit test. The test is now agnostic to the order of elements.
Andres Noetzli [Mon, 14 Sep 2020 15:15:31 +0000 (08:15 -0700)]
Fix type for Windows build (#5062)
The BVToInt preprocessing pass was using uint, which appears to be
undefined when we cross-compile for Windows. This commit fixes the issue
by using size_t.
Andrew Reynolds [Mon, 14 Sep 2020 07:52:28 +0000 (02:52 -0500)]
Standardize uses of inference manager in datatypes (#5035)
Datatypes now has an inference manager. This is work towards making it use the inference manager in all places where it should.
In particular, this makes many of the places where conflicts are determined using `InferenceManager::conflictExp` (explained conflict) instead of `InferenceManager::conflict` + custom calls to explain in TheoryDatatypes. The goal here is to ensure that all explanations from the equality engine are managed by inference manager, which is required for proofs.
Andrew Reynolds [Sat, 12 Sep 2020 03:38:04 +0000 (22:38 -0500)]
(proof-new) Add SMT proof manager (#5054)
This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.
This PR includes setting up some connections into the various modules for proof production.
Andrew Reynolds [Sat, 12 Sep 2020 01:02:33 +0000 (20:02 -0500)]
(proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056)
This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node.
This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR.
Andrew Reynolds [Fri, 11 Sep 2020 21:01:11 +0000 (16:01 -0500)]
Move finite model minimization to UF last call effort (#5050)
This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints).
Fixes #4850.
Andrew Reynolds [Fri, 11 Sep 2020 20:15:53 +0000 (15:15 -0500)]
(proof-new) Handle mismatched assumptions in proof equality engine during mkScope (#5012)
This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases.
A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.
Andrew Reynolds [Fri, 11 Sep 2020 19:38:13 +0000 (14:38 -0500)]
(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)
Previously, strings on proof-new used a ProofStepBuffer for deriving the final conclusion of lemmas in proof equality engine (assertLemma). This was recently changed to use the more standard ProofGenerator interface of assertLemma. However, there was a bug in this method: the steps from this proof need to be deep copied into the proof we are generating or otherwise the explanation of these literals are not connected in the CDProof. This updates the proof equality engine so that it instructs the proof generator to do a deep copy in this case. Notice this is very rarely more than a single step.
Andrew Reynolds [Fri, 11 Sep 2020 00:09:11 +0000 (19:09 -0500)]
Add witness to cvc printer. (#5057)
yoni206 [Thu, 10 Sep 2020 17:23:30 +0000 (10:23 -0700)]
bv2int: refactoring the main translation loop (#5051)
This PR introduces a refactoring of the main translation loop in bv2int preprocessing pass.
Many parts are wrapped by helper functions and so the main loop becomes smaller.
remark: selecting "Hide whitespace changes" cuts the diff by ~50%.
Andrew Reynolds [Thu, 10 Sep 2020 03:34:36 +0000 (22:34 -0500)]
Parser error for wrong number of datatypes (#5049)
Fixes #4973.
yoni206 [Thu, 10 Sep 2020 01:32:55 +0000 (18:32 -0700)]
bv2int: improvement in lazy failures (#5020)
Previously, in case we encountered a term we cannot translate to integers (e.g. a bit-vector array), we would fail.
This PR improves that behavior by keeping the original term, and potentially wrapping it BV_TO_NAT and INT_TO_BV operators.
A test which includes a bit-vector array is included, which was not supported before.
In addition, the treatment of uninterpreted functions is refactored and documented better.
Andrew Reynolds [Thu, 10 Sep 2020 00:19:41 +0000 (19:19 -0500)]
Use state and inference manager in UF CardinalityExtension (#5036)
Previously, the cardinality extension of UF maintained its own (SAT-context-dependent) conflict flag, made custom calls to output channel, and maintained its own cache of lemmas. This standardizes the CardinalityExtension so that it uses state and inference manager of UF, which means that UF and the cardinality extension are fully syncronized concerning whether we are in a conflicting state at all times (d_state.isInConflict). It further cleans up some of the interfaces in CardinalityExtension. This required adding a forwarding method for setIncomplete in inference manager.
Andrew Reynolds [Wed, 9 Sep 2020 22:10:05 +0000 (17:10 -0500)]
(proof-new) Minor changes to proof node updater (#5011)
This includes some changes to proof node updater that are not currently on master.
This includes:
(1) Explicitly passing the result of the current proof node we are updating,
(2) Caching the results of updates based on Node. In other words, proofs (in the same scope) that we have already seen that prove the same thing as the current proof node are reused.
It also enables the compilation of proof post-processor, which was missing on master and makes Rewriter of SmtEngine public which is required for doing so.
Andrew Reynolds [Wed, 9 Sep 2020 20:53:30 +0000 (15:53 -0500)]
(proof-new) Make proofs in term formula removal term context sensitive (#5008)
Previously term formula removal proofs didnt not take the term context into account. This updates it to make use of the term context sensitive support in TConvProofGenerator. More generally, it uses the term context computation as the standard way of caching the results of rewrites in this class (regardless of proofs).
Andrew Reynolds [Wed, 9 Sep 2020 20:11:01 +0000 (15:11 -0500)]
(proof-new) Generalize single step helper in eager proof generator (#5046)
This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.
Andrew Reynolds [Wed, 9 Sep 2020 19:12:52 +0000 (14:12 -0500)]
Fixes for regular expressions + sygus (#5044)
Includes not constructing a default value for non-first class types (e.g. RegLan) and a missing printer case for re.diff.
mudathirmahgoub [Wed, 9 Sep 2020 18:19:40 +0000 (13:19 -0500)]
Add is_singleton operator to the theory of sets (#5033)
This pull request adds a new operator is_singleton for sets to determine whether a set is a singleton.
Before this operator, the user either uses an existential quantifier or the cardinality operator in smtlib. The former affects the performance especially when polarity is negative. The latter requires the cardinality extension in sets theory.
The implementation of is_singleton only uses an internal existential quantifier with the hope of optimizing it later.
New rewriting rules:
(is_singleton (singleton x)) is rewritten as true.
(is_singleton A) is rewritten as (= A (singleton x)) where x is a fresh skolem of the same type of elements of A.
(choose (singleton x)) is rewritten as x.
Andrew Reynolds [Wed, 9 Sep 2020 01:36:08 +0000 (20:36 -0500)]
Split term registry from theory state in sets (#5037)
Currently, the theory state object SolverState in sets sends lemmas and has a reference to the parent theory. This PR is work towards eliminating these dependencies.
This adds a TermRegistry object which is responsible for some of the tasks currently done by SolverState, including all those involving lemmas.
Notice this also makes a bug fix in getUnivSetEqClass where the universe set was being returned instead of its representative.
A followup PR will make SolverState maintain SAT-context-dependent membership lists which is also required for breaking the dependence on the parent theory.
Mathias Preiner [Tue, 8 Sep 2020 18:51:23 +0000 (11:51 -0700)]
Fix printing of fp values. (#5041)
Fixes #5032
Andres Noetzli [Tue, 8 Sep 2020 17:33:59 +0000 (10:33 -0700)]
Make CVC/API BV div/mod semantics match SMT-LIB (#4997)
This commit changes the semantics of the CVC language and with the
default semantics of the API for `BVUDIV`, `BVUREM`, `BVSDIV`, `BVSREM`,
and `BVSMOD` to match the semantics of SMT-LIB >=2.6. Relatedly, the
commit also adds comments to our API documentation for the different
semantics enabled by the `bv-div-zero-const` option.
Andrew Reynolds [Tue, 8 Sep 2020 16:45:38 +0000 (11:45 -0500)]
Eliminate a custom use of TheorySep in quantifiers engine for EPR (#5039)
This moves the initialization of the connection between separation logic and EPR to the separation logic theory, which is a more logical place for this. This eliminates a backwards reference to theory engine from quantifiers engine.
Andrew Reynolds [Fri, 4 Sep 2020 22:52:11 +0000 (17:52 -0500)]
Add asLemma flag to theory inference process (#5030)
This is required for strings, which uses the same data structure, InferInfo, for both lemmas and facts. This ensures the process method of theory inference knows where we are a pending lemma or a pending fact.
It also makes a few changes necessary for the proof-new branch, including disabling the proof node manager in the inference manager for datatypes.