cvc5.git
3 years agoRefactor quantifiers engine initialization (#5813)
Andrew Reynolds [Tue, 26 Jan 2021 18:43:50 +0000 (12:43 -0600)]
Refactor quantifiers engine initialization (#5813)

This is a step towards breaking up the quantifiers engine.

The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.

This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.

3 years agoReestablishing support for define-sort (#5810)
Haniel Barbosa [Tue, 26 Jan 2021 16:10:33 +0000 (13:10 -0300)]
Reestablishing support for define-sort (#5810)

Presumable broken since 3ed42d7ab. This extends the API to have a substitute method for Sort that in needed for doing the Sort substitution in the case of define-sort.

This fixes issue #5809.

3 years agoAdd proofs to TheoryArithPrivate::propagate (#5812)
Alex Ozdemir [Tue, 26 Jan 2021 04:20:58 +0000 (20:20 -0800)]
Add proofs to TheoryArithPrivate::propagate (#5812)

Specifically, add proofs to conflicts between (a) a propagation from the
congruence manager and (b) a constraint from the main solver.

3 years agoRefactor bags::SolverState (#5783)
mudathirmahgoub [Mon, 25 Jan 2021 20:38:45 +0000 (14:38 -0600)]
Refactor bags::SolverState (#5783)

Couple of changes:

SolverState now keep tracks of elements per bag instead of per type.
bags::InferInfo now stores multiple conclusions (conjuncts).
BagSolver applies upward/downward closures for bag elements

3 years agoEnsure uses of ground terms in triggers are preprocessed and registered (#5808)
Andrew Reynolds [Mon, 25 Jan 2021 17:11:02 +0000 (11:11 -0600)]
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)

This ensures ground terms in triggers are preprocessed and registered in the master equality engine. This avoids cases where our E-matching algorithm is incomplete where it should not be.

Positive impact (+222-69) on SMT-LIB, 30 second timeout

3 years agoSplit inst match generator into multiple files (#5805)
Andrew Reynolds [Mon, 25 Jan 2021 16:29:39 +0000 (10:29 -0600)]
Split inst match generator into multiple files (#5805)

No code changes on this PR, only move + format.

3 years agoSplit E-matching strategies to own files (#5807)
Andrew Reynolds [Mon, 25 Jan 2021 14:59:18 +0000 (08:59 -0600)]
Split E-matching strategies to own files (#5807)

Code move + format only

3 years agorename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)
mudathirmahgoub [Mon, 25 Jan 2021 00:18:12 +0000 (18:18 -0600)]
rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)

Rename strings::InferInfo::d_newSkolem to InferInfo::d_skolems to match bags::InferInfo:d_skolems

3 years ago Initial cleaning of e-matching instantiation strategy (#5796)
Andrew Reynolds [Sun, 24 Jan 2021 19:55:50 +0000 (13:55 -0600)]
 Initial cleaning of e-matching instantiation strategy (#5796)

In preparation for splitting this into multiple files.

No behavior changes in this PR.

3 years agoInitial cleaning of triggers (#5795)
Andrew Reynolds [Sun, 24 Jan 2021 19:13:06 +0000 (13:13 -0600)]
Initial cleaning of triggers (#5795)

In preparation for splitting trigger.h/cpp into multiple files.

This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified.

3 years agoInitial cleaning of inst match generator (#5794)
Andrew Reynolds [Sun, 24 Jan 2021 18:43:54 +0000 (12:43 -0600)]
Initial cleaning of inst match generator (#5794)

In preparation towards breaking this file up into multiple files.

No code changes, only updates to conform to new guidelines.

3 years ago(proof-new) Instantiation list utility (#5768)
Andrew Reynolds [Sun, 24 Jan 2021 18:12:10 +0000 (12:12 -0600)]
(proof-new) Instantiation list utility (#5768)

This is in preparation for refactoring the printing of instantiations. We will migrate the printing of instantiations (currently done in the Instantiate module within quantifiers engine) to somewhere more high level e.g. the SmtEngine or in the command layer. This will make the infrastructure for dumping instantiations much more flexible, as implemented on proof-new.

3 years agoAdd interface for getting preprocessed term (#5798)
Andrew Reynolds [Sun, 24 Jan 2021 17:42:08 +0000 (11:42 -0600)]
Add interface for getting preprocessed term (#5798)

Several places, e.g. in quantifiers, requiring knowing what the theory-preprocessed form of a node is.

This is required for an improvement to our E-matching algorithm, which requires knowing what the preprocessed form of ground subterms of triggers are.

Note that I'm not 100% happy with adding a new interface to Valuation, but at the moment I don't see a better way of doing this. On the positive side, this interface will make a few other things (e.g. the return value of OutputChannel::lemma) obsolete.

3 years ago[proof-new] Expanding MACRO_RESOLUTION in post-processing (#5755)
Haniel Barbosa [Fri, 22 Jan 2021 16:15:43 +0000 (13:15 -0300)]
[proof-new] Expanding MACRO_RESOLUTION in post-processing (#5755)

Breaks down resolution, factoring and reordering. The hardest part of this process is making getting rid of the so-called "crowding literals", i.e., duplicate literals introduced during the series of resolutions and removed implicitly by the SAT solver. A naive removal via addition of premises to the chain resolution can lead to exponential behavior, so instead the removal is done by breaking the resolution and applying a factoring step midway through. This guarantees non-exponential behavior.

3 years agoAdd div, mod, abs in non-strict parsing mode (#5793)
Andrew Reynolds [Thu, 21 Jan 2021 18:07:50 +0000 (12:07 -0600)]
Add div, mod, abs in non-strict parsing mode (#5793)

The recent change to the parser currently breaks our performance on several critical applications, including the use of CVC4 in Facebook. We should only throw a parse error for div in linear logics when strict mode is enabled.

3 years agoarith: Proofs for Diophantine cuts (#5792)
Alex Ozdemir [Thu, 21 Jan 2021 04:30:56 +0000 (20:30 -0800)]
arith: Proofs for Diophantine cuts (#5792)

Thread proofs through the diophantine "cutting" lemma generator.

3 years agoRefactoring the single invocation solver (#5706)
Andrew Reynolds [Wed, 20 Jan 2021 23:32:06 +0000 (17:32 -0600)]
Refactoring the single invocation solver (#5706)

This does an intermediate refactoring of the single invocation solver to make a few things clearer and to add preliminary support for functions that have been marked as solved by external techniques.

This is in preparation for generalizing the CAV 2015 single invocation techniques.

3 years agoFix type issues with relevant domain computation (#5788)
Andrew Reynolds [Wed, 20 Jan 2021 21:56:26 +0000 (15:56 -0600)]
Fix type issues with relevant domain computation (#5788)

This fixes 2 issues with relevant domain type computation, the first involving arithmetic INST_CONSTANT that do not belong to the current quantified formula being solved for in a monomial sum, the second involving parametric datatype selectors.

Fixes #5635. Both benchmarks on that issue are unsolved (one timeout, one unknown) but throw no assertion failure.

3 years agoFix corner case of wrongly applied selector as trigger (#5786)
Andrew Reynolds [Wed, 20 Jan 2021 18:59:13 +0000 (12:59 -0600)]
Fix corner case of wrongly applied selector as trigger (#5786)

Fixes #5766.

3 years agoDo not track processed in remove term formulas loop (#5791)
Andrew Reynolds [Wed, 20 Jan 2021 15:56:02 +0000 (09:56 -0600)]
Do not track processed in remove term formulas loop (#5791)

The assertion/tracking was spurious, since an eliminated term may occur in multiple contexts.

Fixes #5728 (which I could not reproduce currently). Adds a regression from a duplicate of that issue.

3 years agoSMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)
Aina Niemetz [Wed, 20 Jan 2021 15:28:29 +0000 (07:28 -0800)]
SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)

This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.

More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.

3 years agoUse arbitrary ground term assignment for sorts where isInterpretedFinite is true...
Andrew Reynolds [Wed, 20 Jan 2021 01:28:08 +0000 (19:28 -0600)]
Use arbitrary ground term assignment for sorts where isInterpretedFinite is true (#5790)

This makes a small change to our model construction to assign arbitrary values to eqc for types that are "interpreted finite", that is, have finite cardinality under the assumption that uninterpreted sorts are finite/infinite (when finite model finding is on/off). Uninterpreted sorts themselves always use the type enumerator to assign distinct values.

This fixes #5738.

This change is necessary since there was previously a mismatch between types where isFinite != isInterpretedFinite, in particular a datatype with a single constructor with a unintepreted type field as in that issue.

3 years agoImplement proofs for arith BRAB lemmas (#5784)
Alex Ozdemir [Tue, 19 Jan 2021 22:25:02 +0000 (14:25 -0800)]
Implement proofs for arith BRAB lemmas (#5784)

All changes:

Add a Pf type alias for std::shared_ptr to
expr/proof_rule.h
Add an eager proof generator to TheoryArith for preprocessing
rewrites. Right now those are proven with INT_TRUST. Will eventually
fix.
Generate proved lemmas in TheoryArithPrivate::branchIntegerVariable.
Same for TheoryArithPrivate::roundRobinBranch
Add EagerProofGenerator::mkTrustedRewrite.
Add some proofsEnabled methods.

3 years agoImplement --no-strings-lazy-pp as a preprocessing pass (#5777)
Andrew Reynolds [Fri, 15 Jan 2021 21:19:43 +0000 (15:19 -0600)]
Implement --no-strings-lazy-pp as a preprocessing pass (#5777)

This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.

Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.

3 years agoUpdates to theory preprocess equality (#5776)
Andrew Reynolds [Thu, 14 Jan 2021 13:28:55 +0000 (07:28 -0600)]
Updates to theory preprocess equality (#5776)

This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.

For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.

The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.

3 years agoSplit eager solver from strings solver state (#5775)
Andrew Reynolds [Wed, 13 Jan 2021 22:01:53 +0000 (16:01 -0600)]
Split eager solver from strings solver state (#5775)

This splits the eager solver from solver state. The solver state contains the EqcInfo data, while the eager solver is responsible for populating it.

This is in preparation for adding new techniques to the eager solver.

No behavior changes in this PR, only reorganization.

3 years agoAdd unit test for api getInterpolant() -- issue #5593 (#5772)
Ying Sheng [Wed, 13 Jan 2021 19:19:45 +0000 (03:19 +0800)]
Add unit test for api getInterpolant() -- issue #5593 (#5772)

The pull request addressed issue #5593 for adding an unit test.

3 years agoDo not call ppRewrite on Boolean equalities (#5762)
Andrew Reynolds [Wed, 13 Jan 2021 14:28:56 +0000 (08:28 -0600)]
Do not call ppRewrite on Boolean equalities (#5762)

Was causing arithmetic to process a Boolean equality when --arith-rewrite-equalities is true.

Fixes #5761.

3 years agogoogle test: expr: Migrate node_black. (#5764)
Aina Niemetz [Tue, 12 Jan 2021 17:36:46 +0000 (09:36 -0800)]
google test: expr: Migrate node_black. (#5764)

3 years agogoogle test: Use ASSERT_* instead of EXPECT_*. (#5765)
Aina Niemetz [Tue, 12 Jan 2021 16:55:56 +0000 (08:55 -0800)]
google test: Use ASSERT_* instead of EXPECT_*. (#5765)

Use ASSERT instead of EXPECT for consistency. There's no real benefit
for us to use EXPECT -- the main difference is that within a test,
EXPECT failures do not terminate the test, while ASSERT failures do.

This further fixes a minor issue in theory_sets_type_rules_white.h
(which is still not migrated to google test yet).

3 years agoForeign theory rewrite option (#5763)
yoni206 [Tue, 12 Jan 2021 15:42:37 +0000 (07:42 -0800)]
Foreign theory rewrite option (#5763)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the third and final step. It adds the user-facing option that turn this feature on, as well as regression tests.

3 years agoMerge theory registrar and theory proxy (#5758)
Andrew Reynolds [Mon, 11 Jan 2021 17:23:15 +0000 (11:23 -0600)]
Merge theory registrar and theory proxy (#5758)

The motivation of this PR is to make TheoryProxy the single point of contact to TheoryEngine from PropEngine.

This merges the helper class TheoryRegistrar into TheoryProxy.

3 years agoFurther simplifications in preparation for removing Expr layer (#5756)
Andrew Reynolds [Mon, 11 Jan 2021 15:46:28 +0000 (09:46 -0600)]
Further simplifications in preparation for removing Expr layer (#5756)

This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.

These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.

This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.

3 years agoRemove extended rewrite for arithmetic (#5760)
Andrew Reynolds [Mon, 11 Jan 2021 14:48:01 +0000 (08:48 -0600)]
Remove extended rewrite for arithmetic (#5760)

This rewrite is no longer needed since our philosophy on rewriting extended arithmetic symbols has changed (we employ aggressive rewriting for extended arithmetic symbols in the normal rewriter). Moreover there was a soundness bug in the extended rewriter for division and mod by 0.

Fixes #5737, fixes #5740.

3 years agoStrings arith checks preprocessing pass: step 2 (#5750)
yoni206 [Sat, 9 Jan 2021 14:35:18 +0000 (06:35 -0800)]
Strings arith checks preprocessing pass: step 2 (#5750)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the second step. It includes the implementation of the main function, as well as unit tests for it.

A subsequent PR will add a user-level option that will turn on this preprocessing pass, as well as regression tests.

3 years agoFix issue 5513 (#5757)
mudathirmahgoub [Sat, 9 Jan 2021 14:10:07 +0000 (08:10 -0600)]
Fix issue 5513 (#5757)

Fix issue5513 by throwing an exception for unsupported bag operators

3 years agoRename getAntecedent to getPremises (#5754)
mudathirmahgoub [Fri, 8 Jan 2021 17:07:32 +0000 (11:07 -0600)]
Rename getAntecedent to getPremises (#5754)

Changes:

renamed d_new_skolem to d_newSkolem
renamed d_ant to d_premises (antecedent is usually used with consequent, and premise is used with conclusion)

3 years ago[proof-new] Implementing getProof in the API and SMT engine (#5751)
Haniel Barbosa [Fri, 8 Jan 2021 16:38:24 +0000 (13:38 -0300)]
[proof-new]  Implementing getProof in the API and SMT engine (#5751)

A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).

3 years agoAdd bags inference generator (#5731)
mudathirmahgoub [Fri, 8 Jan 2021 16:07:50 +0000 (10:07 -0600)]
Add bags inference generator  (#5731)

This PR adds inference generator for basic bag rules.

3 years agobv-to-int: avoid binarizing nodes twice (#5749)
yoni206 [Fri, 8 Jan 2021 15:08:05 +0000 (07:08 -0800)]
bv-to-int: avoid binarizing nodes twice (#5749)

In bv-to-int, we first binarize the applications of associative-commutative operators (like bvadd etc.).
With this PR, we first check whether we already binarized a node, and only if we didn't, we perform binarization.

3 years agoMake sure polynomials are properly factorized in nl-cad (#5733)
Gereon Kremer [Thu, 7 Jan 2021 21:55:31 +0000 (22:55 +0100)]
Make sure polynomials are properly factorized in nl-cad (#5733)

CAD theory (used in nl-cad) requires that polynomials are properly factorized (a finest square-free basis). This PR replaces usage of raw std::vector by a new wrapper PolyVector that ensures proper factorization whenever a polynomial is added. This fixes one piece of code that omitted factorization, leading to soundness issues as in #5726.
Fixes #5726.

3 years agoRemove dependency on expression layer in TPTP parser (#5753)
Haniel Barbosa [Thu, 7 Jan 2021 21:10:05 +0000 (18:10 -0300)]
Remove dependency on expression layer in TPTP parser (#5753)

3 years agoFix warning in TPTP parser (#5752)
Haniel Barbosa [Thu, 7 Jan 2021 20:06:33 +0000 (17:06 -0300)]
Fix warning in TPTP parser  (#5752)

3 years agostrings arith checks preprocessing pass: step 1 (#5747)
yoni206 [Wed, 6 Jan 2021 22:41:13 +0000 (14:41 -0800)]
strings arith checks preprocessing pass: step 1 (#5747)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the first step. It only includes the preprocessing pass infrastructure, with an empty implementation of the main function StrLenSimplify::simplify. It also adds the pass to the registry.
The implementation of this function is not complicated, but is left for a future PR in order to keep the PR short.

Future PRs will include an implementation of the main function, tests, and a command line option to turn on the pass.

3 years agoAdd new interfaces to term formula removal and theory preprocess (#5717)
Andrew Reynolds [Wed, 6 Jan 2021 01:40:12 +0000 (19:40 -0600)]
Add new interfaces to term formula removal and theory preprocess (#5717)

This is in preparation for lazy lemmas for term formula removal.

3 years agoAdding str.len to triggers (#5746)
yoni206 [Tue, 5 Jan 2021 19:19:34 +0000 (11:19 -0800)]
Adding str.len to triggers (#5746)

This PR adds str.len to symbols that are considered for instantiations.
It is motivated by a benchmark that originated from Boogie.
A minimized version of that benchmark is added as a regression.

3 years agoRemove a few miscellaneous references to the expr layer (#5661)
Andrew Reynolds [Tue, 5 Jan 2021 16:07:07 +0000 (10:07 -0600)]
Remove a few miscellaneous references to the expr layer (#5661)

Leftover from a development branch.

3 years ago[proof-new] Only use old proofs for unsat cores if no proof new (#5725)
Haniel Barbosa [Thu, 24 Dec 2020 04:15:40 +0000 (01:15 -0300)]
[proof-new] Only use old proofs for unsat cores if no proof new (#5725)

Now the old proofs are used for unsat cores only if proofNew is disabled. Later commits will generate unsat cores from the new proofs when requested. Eventually we will compare them and when we confirm the new unsat core generation is better we will delete the old one.

This also does some minor refactoring in some preprocessing. No behavior is changed.

3 years agoDumping unsat cores after check-sat-assuming/QUERY (#5724)
Haniel Barbosa [Wed, 23 Dec 2020 23:10:34 +0000 (20:10 -0300)]
Dumping unsat cores after check-sat-assuming/QUERY (#5724)

Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.

It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.

3 years agoAdd option to track and notify from CNF stream (#5708)
Andrew Reynolds [Wed, 23 Dec 2020 22:17:48 +0000 (16:17 -0600)]
Add option to track and notify from CNF stream (#5708)

This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals).

This will be required for SAT relevancy.

No behavior changes in this PR.

3 years agoRemove quant EPR option (#5716)
Andrew Reynolds [Wed, 23 Dec 2020 21:26:24 +0000 (15:26 -0600)]
Remove quant EPR option (#5716)

This was an experimental option used in combination with separation logic.

3 years ago[proof-new] Adding a manager for the new unsat cores (#5723)
Haniel Barbosa [Wed, 23 Dec 2020 20:40:48 +0000 (17:40 -0300)]
[proof-new] Adding a manager for the new unsat cores (#5723)

Based on proof nodes of refutations.

3 years ago(proof-new) Miscelleneous fixes from proof-new (#5714)
Andrew Reynolds [Wed, 23 Dec 2020 20:13:03 +0000 (14:13 -0600)]
(proof-new) Miscelleneous fixes from proof-new (#5714)

3 years agoAdd proofs for nonlinear sign lemmas. (#5707)
Gereon Kremer [Wed, 23 Dec 2020 03:40:45 +0000 (04:40 +0100)]
Add proofs for nonlinear sign lemmas. (#5707)

This PR adds proof support for NL_SIGN lemmas.

3 years agoMinor simplification to Theory::theoryOf (#5719)
Andrew Reynolds [Wed, 23 Dec 2020 03:23:15 +0000 (21:23 -0600)]
Minor simplification to Theory::theoryOf (#5719)

This removes the special case of constants based on the observation that the theory that owns the type of a constant and the theory that owns its kind always should be the same.

This should lead to a small (maybe 1%) performance improvement, as this method is run ~191M times in our coverage build.

3 years agoDelete duplicated code (#5718)
yoni206 [Tue, 22 Dec 2020 23:17:27 +0000 (15:17 -0800)]
Delete duplicated code (#5718)

3 years agoMove slow regression to regress3 (#5715)
Andrew Reynolds [Tue, 22 Dec 2020 20:07:19 +0000 (14:07 -0600)]
Move slow regression to regress3 (#5715)

3 years agoMake theory preprocess rewrite equalities a preprocessing pass (#5711)
Andrew Reynolds [Tue, 22 Dec 2020 14:24:24 +0000 (08:24 -0600)]
Make theory preprocess rewrite equalities a preprocessing pass (#5711)

Some theories rewrite equalities during ppRewrite. An example is arithmetic with the option arith-rewrite-eq, which rewrites (= x y) to (and (>= x y) (<= x y)) during theory preprocessing.

This PR makes it so that ppRewrite is only called on equalities in preprocessing, during a new preprocessing pass "TheoryRewriteEq". On the other hand, ppRewrite is never called on new equalities generated in lemmas from TheoryEngine.

In detail, the motivation for this change:

(1) Rewriting equalities during ppRewrite is dangerous since it may break invariants wrt theory combination. In particular, equalities in splitting lemmas originating from theory combination must not be theory-preprocessed, or else we may be non-terminating or solution unsound. This can happen if a theory requests a split on (= x y) but is not notified of this atom when another theory rewrites (= x y) during ppRewrite.

(2) After this PR, we can simplify our policy for all lemmas generated, in particular, we can say that all lemmas must be theory preprocessed before their literals are asserted to TheoryEngine. This is now possible as the invariant cannot be broken (theoryRewriteEq is relegated to the preprocessor, which is only applied once). This will make LemmaProperty::PREPROCESS obsolete, which in turn will simplify several lemma caches for nonlinear and quantifiers. It will also significantly simplify proof production for the theory preprocessor (which maintains two stacks of utilities for preprocessed vs non-preprocessed lemmas).

(3) Simplifications to the above policy will make it significantly easier to implement theory-preprocessing apply when literals are asserted. It is currently not possible to implement this in a coherent way without tracking which literals were a part of lemmas marked as "do not theory-preprocess".

3 years agoRemove preregister instantiation heuristic (#5713)
Andrew Reynolds [Tue, 22 Dec 2020 07:49:28 +0000 (01:49 -0600)]
Remove preregister instantiation heuristic (#5713)

This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.

3 years agoAdd proof for pi bound lemma (#5709)
Gereon Kremer [Mon, 21 Dec 2020 19:49:24 +0000 (20:49 +0100)]
Add proof for pi bound lemma (#5709)

This PR adds proofs for lemmas that introduce bounds on the constant representing pi.

3 years agoHave unsat core regression agnostic to number of assertions in core (#5712)
Haniel Barbosa [Mon, 21 Dec 2020 19:17:13 +0000 (16:17 -0300)]
Have unsat core regression agnostic to number of assertions in core (#5712)

Changing our unsat core infrastructure may change the cores we produce. This can be problematic for regressions that hardcode the number of assertions we get (such as this one). This commit changes such a regression to rather expect any core. It is motivated by exactly the previously described issue occurring after using the new proof infrastructure to generate unsat cores, which yielded a smaller core.

Kudos to @4tXJ7f for the sed magic.

3 years agoMove ownership of theory preprocessor to TheoryProxy (#5690)
Andrew Reynolds [Mon, 21 Dec 2020 17:48:22 +0000 (11:48 -0600)]
Move ownership of theory preprocessor to TheoryProxy (#5690)

With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.

No significant behavior changes in this PR.

The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.

3 years agoAdd proof for sine shift lemmas. (#5710)
Gereon Kremer [Mon, 21 Dec 2020 17:16:53 +0000 (18:16 +0100)]
Add proof for sine shift lemmas. (#5710)

This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and pi.

3 years ago(proof-new) Make nl-ext factoring lemmas proof producing. (#5698)
Gereon Kremer [Mon, 21 Dec 2020 16:20:23 +0000 (17:20 +0100)]
(proof-new) Make nl-ext factoring lemmas proof producing. (#5698)

This PR adds proofs for the lemmas from the nonlinear factoring check.

3 years agoEliminate recursion from the internals of term formula removal (#5701)
Andrew Reynolds [Mon, 21 Dec 2020 14:53:41 +0000 (08:53 -0600)]
Eliminate recursion from the internals of term formula removal (#5701)

This makes all recursion (applying term formula removal on lemmas introduced by term formula removal) optionally happen at the top level call.

This is in preparation for making term formula removal lazier, in which case we will only apply one step of term formula removal at a time.

One QF_UFNIA regression times out due to changing the search, an option is changed for this benchmark.

3 years agoFix issue with selector triggers (#5689)
Andrew Reynolds [Mon, 21 Dec 2020 13:55:34 +0000 (07:55 -0600)]
Fix issue with selector triggers (#5689)

Code could segfault if the number of wrongly applied selector applications was different from correctly applied ones.

3 years ago(proof-new) Setup proof infrastructure for transcendental solver (#5703)
Gereon Kremer [Fri, 18 Dec 2020 17:11:51 +0000 (18:11 +0100)]
(proof-new) Setup proof infrastructure for transcendental solver (#5703)

This PR introduces the infrastructure for adding proofs to the transcendental solver:

a CDProofSet to easily create new proofs
a proof checker

3 years agoSimplify internal API for sygus (#5687)
Andrew Reynolds [Fri, 18 Dec 2020 16:01:17 +0000 (10:01 -0600)]
Simplify internal API for sygus (#5687)

This makes simplifications to the internal sygus API now that the SmtEngine interface is independent of parsing.

3 years agoAdd proof checker for nl tangent lemma (#5704)
Gereon Kremer [Fri, 18 Dec 2020 15:25:06 +0000 (16:25 +0100)]
Add proof checker for nl tangent lemma (#5704)

This PR is a follow-up to #5700 which lacked the proof checker for the proof that was added for nonlinear tangent plane lemmas.

3 years agoBugfix: proofs for props of non-normal arith lits (#5702)
Alex Ozdemir [Fri, 18 Dec 2020 15:01:58 +0000 (07:01 -0800)]
Bugfix: proofs for props of non-normal arith lits  (#5702)

Arith has a normal form for literals, which the rewriter computes.

Nonetheless, arith sometimes gets (and ultimately propagates) non-normal
literals. It normalizes them internally and goes about its business.

However, when asked for an explanation, it must prove the non-normal
literal, rather than the normal one.

Also includes a regression for the bug, courtesy of Andy.

Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
3 years ago(proof-new) Add proof for tangent plane lemmas (#5700)
Gereon Kremer [Fri, 18 Dec 2020 07:59:43 +0000 (08:59 +0100)]
(proof-new) Add proof for tangent plane lemmas (#5700)

This PR adds a proof for the tangent plane lemmas from nl-ext.
As this lemma uses some insight about the tangent plane of a multiplication term, this PR adds a new proof rule.

3 years agoAdd proof for split zero check. (#5699)
Gereon Kremer [Fri, 18 Dec 2020 07:26:55 +0000 (08:26 +0100)]
Add proof for split zero check. (#5699)

This PR adds a proof for the nl-ext check to split at zero. As we can use the SPLIT rule, this requires no new proof rule.

3 years ago(proof-new) Minor updates to term conversion proof generator (#5691)
Andrew Reynolds [Thu, 17 Dec 2020 16:50:49 +0000 (10:50 -0600)]
(proof-new) Minor updates to term conversion proof generator (#5691)

Minor updates to term conversion proof generator

3 years agoAlways consider rewritten lemmas for caching. (#5696)
Gereon Kremer [Thu, 17 Dec 2020 16:28:10 +0000 (17:28 +0100)]
Always consider rewritten lemmas for caching. (#5696)

The TheoryInferenceManager cached lemmas as they came in. This PR always rewrites before consulting the cache, making caching more consistent and robust. This change is coming in from proof-new.

3 years ago(proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697)
Gereon Kremer [Thu, 17 Dec 2020 16:12:15 +0000 (17:12 +0100)]
(proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697)

This PR prepares the nonlinear extension itself and the nl-ext part for proofs. In particular

    we add a proof checker for nl-ext
    we add a CDProofSet for nl-ext

3 years agoSimplify term formula removal interface (#5695)
Andrew Reynolds [Thu, 17 Dec 2020 15:19:20 +0000 (09:19 -0600)]
Simplify term formula removal interface (#5695)

This no longer needs some methods that were previously used specifically for ITE preprocessing and check-model.

3 years agoSimplify and fix check models (#5685)
Andrew Reynolds [Thu, 17 Dec 2020 09:10:39 +0000 (03:10 -0600)]
Simplify and fix check models (#5685)

Currently --check-models is implemented by replaying several preprocessing steps, including theory-specific expand definitions, and then checking whether the result evaluates to true.

However, by having --check-models rely on complex preprocessing machinery defeats its purpose, as these steps are part of its trusted base.

Moreover, issue #5645 demonstrates that this may lead to spurious errors where we incorrectly conclude that an input assertion is false, when it is not.

This PR significantly simplifies --check-models so that it only relies on define-fun expansion + rewriting + evaluation. This ensures that --check-models is "sound" i.e. it does not falsely report a formula as evaluating to false. As a consequence, this makes check-models give warnings more often, i.e. when partial operators are involved, thus -q is added to silence warnings on some regressions.

A followup PR will use a satisfiability check on the input formula post-expand-definitions to properly implement a trustworthy version of check-models that is robust for partial operators.

Fixes #5645.

3 years ago[proof-new] Only use old proof code for unsat cores if new proofs are off (#5688)
Haniel Barbosa [Thu, 17 Dec 2020 00:16:28 +0000 (21:16 -0300)]
[proof-new] Only use old proof code for unsat cores if new proofs are off (#5688)

This is so that eventually we can compare the performance of the old unsat cores vs the new ones.

3 years agoSimplify preprocessing (#5647)
Andrew Reynolds [Wed, 16 Dec 2020 22:35:59 +0000 (16:35 -0600)]
Simplify preprocessing (#5647)

This simplifies preprocessing so that the only call to theory-preprocess and ite-removal is at the very end. (One exception is early-theory-pp which is used by default in combination with ite-simp to maintain the performance on QF_LIA/nec).

This is in preparation for making theory preprocessing happen lazily, post-CNF conversion.

@HanielB has done SMT-LIB performance runs, see below.

3 years agoMark quantifier instantiations as needs justify (#5684)
Andrew Reynolds [Wed, 16 Dec 2020 21:07:55 +0000 (15:07 -0600)]
Mark quantifier instantiations as needs justify (#5684)

This avoids a solution soundness issue when disabling all NL strategies and using --nl-rlv=always.

3 years agoSimplify synth-fun printer (#5682)
Andrew Reynolds [Wed, 16 Dec 2020 20:02:58 +0000 (14:02 -0600)]
Simplify synth-fun printer (#5682)

Simplifies synth-fun printing to assume that the function-to-synthesize should be printed with the proper name and return type.

3 years agoRenamed InferInfo::getAntecedant to InferInfo::getAntecedent (#5683)
mudathirmahgoub [Wed, 16 Dec 2020 19:22:59 +0000 (13:22 -0600)]
Renamed InferInfo::getAntecedant to InferInfo::getAntecedent (#5683)

Renamed InferInfo::getAntecedant to InferInfo::getAntecedent

3 years ago(proof-new) Use bound variable manager (#5679)
Andrew Reynolds [Wed, 16 Dec 2020 16:52:26 +0000 (10:52 -0600)]
(proof-new) Use bound variable manager (#5679)

This uses BoundVarManager for several key places where bound variables are introduced, including for array extensionality witness terms, string preprocessing, quantifiers rewriting, and skolemization.

This is motivated by making certain steps in solving deterministic for the sake of proofs, and gives a more consistent pattern in general for constructing bound variables.

3 years agoMove ownership of term formula removal to theory preprocessor (#5670)
Andrew Reynolds [Wed, 16 Dec 2020 15:03:45 +0000 (09:03 -0600)]
Move ownership of term formula removal to theory preprocessor (#5670)

This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion.

This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move.

The next step will move the TheoryPreprocessor inside prop::TheoryProxy.

There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.

3 years agoUse uint64 utility when parsing tuple selectors in smt2 (#5681)
Andrew Reynolds [Wed, 16 Dec 2020 09:33:03 +0000 (03:33 -0600)]
Use uint64 utility when parsing tuple selectors in smt2 (#5681)

The smt2 parser is now 100% independent from the Expr-layer.

3 years agoMove trigger trie to own file (#5680)
Andrew Reynolds [Tue, 15 Dec 2020 23:55:06 +0000 (17:55 -0600)]
Move trigger trie to own file (#5680)

Also updates minor things to meet coding standards and makes it so that children in the trie are not dynamically allocated.

3 years agoImprovements related to quantifiers printing (#5678)
Andrew Reynolds [Tue, 15 Dec 2020 23:16:07 +0000 (17:16 -0600)]
Improvements related to quantifiers printing (#5678)

Also fixes a bug where patterns would be printed with the wrong scope (that included the bound variable list).

3 years agoProper expand definitions for sets (#5676)
Andrew Reynolds [Tue, 15 Dec 2020 21:55:38 +0000 (15:55 -0600)]
Proper expand definitions for sets (#5676)

In the new view, expandDefinitions is used for eliminating partial operators and is not called during solving, and ppRewrite is called during preprocessing.

For sets, choose is a partial operator that should be applied in expand definitions, and in ppRewrite. On the other hand, is_singleton should not be expanded in expandDefinitions since it is not a partial operator, so it should only be handled in ppRewrite.

It also removes some outdated documentation regarding expandDefinitions with universe set, which is now handled by preventing universe set from occurring in solved substitutions.

This is in preparation for refactoring check-model.

3 years agoConsolidate basic sygus utilities regarding sygus conjectures (#5421)
Andrew Reynolds [Tue, 15 Dec 2020 21:19:08 +0000 (15:19 -0600)]
Consolidate basic sygus utilities regarding sygus conjectures (#5421)

This is required for new work on generalizing CAV 2015 single invocation techniques.

It adds a new system of marking solutions for synthesis conjectures as attributes, which will be used as a way of eliminating functions from a conjecture while still preserving their solution in a response to check-synth.

3 years agoFix datatypes compute ground value (#5671)
Andrew Reynolds [Tue, 15 Dec 2020 20:49:33 +0000 (14:49 -0600)]
Fix datatypes compute ground value (#5671)

We were using the wrong cache on one call, leading to non-constant values being enumerated.

Fixes #5659, for that benchmark, CVC4 now answers "unknown".

3 years agoRemove bv divide by zero option (#5672)
Andrew Reynolds [Tue, 15 Dec 2020 20:04:27 +0000 (14:04 -0600)]
Remove bv divide by zero option (#5672)

This is required to avoid failures in the planned refactoring of check-models.

This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem.

It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM.

FYI @barrettcw

3 years agoAdd getters to retrieve constants from api::Term (#5677)
Gereon Kremer [Tue, 15 Dec 2020 19:09:54 +0000 (20:09 +0100)]
Add getters to retrieve constants from api::Term (#5677)

This PR adds method to obtain constant values from api::Term that are either integers or strings.

3 years ago[proof-new] Making the CDCL(T) Minisat proof producing (#5669)
Haniel Barbosa [Mon, 14 Dec 2020 23:39:58 +0000 (20:39 -0300)]
[proof-new] Making the CDCL(T) Minisat proof producing (#5669)

This closely follows the old proof code in terms of where Minisat is hooked to the SatProofManager, other than a few places like registering removed clauses and removal of redundant literals. Note that this together with the thorough handling from SatProofManager makes the new SAT proofs perceptibly more robust than the old ones.

This PR also adds some traces to better track what Minisat does.

3 years ago[proof-new] Make prop engine proof producing (#5667)
Haniel Barbosa [Mon, 14 Dec 2020 19:06:47 +0000 (16:06 -0300)]
[proof-new] Make prop engine proof producing (#5667)

3 years agoProperly implement datatype selector triggers (#5624)
Andrew Reynolds [Mon, 14 Dec 2020 17:38:04 +0000 (11:38 -0600)]
Properly implement datatype selector triggers (#5624)

This ensures that datatype selectors are properly handled as triggers in E-matching.

This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.

It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).

This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.

Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.

FYI @barrettcw

3 years ago[proof-new] Updating interfaces between prop engine and minisat (#5664)
Haniel Barbosa [Mon, 14 Dec 2020 16:14:59 +0000 (13:14 -0300)]
[proof-new] Updating interfaces between prop engine and minisat (#5664)

This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface".

Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code.

3 years ago(proof-new) Add bound variable manager (#5655)
Andrew Reynolds [Mon, 14 Dec 2020 15:39:13 +0000 (09:39 -0600)]
(proof-new) Add bound variable manager (#5655)

This is a common utility for constructing canonical bound variables.

3 years agoFix and improve evaluator (#5563)
Andrew Reynolds [Mon, 14 Dec 2020 14:35:28 +0000 (08:35 -0600)]
Fix and improve evaluator (#5563)

This fixes a segfault in the evaluator for substitutions of the form x -> t where t is not constant.

This consolidates 2 cases where we did not evaluate children (when we are variable or are an application term with an unevaluated child). This was problematic previously since we would access children of currNode instead of currNodeVal.

This also makes our handling of APPLY_UF more consistent, so that it is added to the main switch statement.

3 years agoFix SAT-context dependent issue in strings preregistration (#5564)
Andrew Reynolds [Mon, 14 Dec 2020 13:04:17 +0000 (07:04 -0600)]
Fix SAT-context dependent issue in strings preregistration (#5564)

This makes preregistration of terms SAT-context dependent in strings instead of user-context dependent.

Fixes #5547.

This is required to avoid model unsoundness on sequence benchmarks, as demonstrated in that issue.

It furthermore impacts how we have been handling theory combination with arithmetic for str.len and impacts how propagation is setup for the strings equality engine.

I will do performance testing on this PR.

3 years agoFlush statistics through NodeManager in SmtEngine (#5652)
Andrew Reynolds [Sat, 12 Dec 2020 04:54:50 +0000 (22:54 -0600)]
Flush statistics through NodeManager in SmtEngine (#5652)

This removes the dependency on the Expr layer from src/main.

This requires moving the flushing of NodeManager statistics within SmtEngine.

This is a temporary solution until we have a permanent solution for statistics.