cvc5.git
2 years agodocs: Do not use explicit line numbers in literalinclude. (#8690)
Aina Niemetz [Mon, 2 May 2022 20:13:00 +0000 (13:13 -0700)]
docs: Do not use explicit line numbers in literalinclude. (#8690)

2 years agoFurther refactoring in preparation for CONST_INTEGER (#8687)
Andrew Reynolds [Mon, 2 May 2022 19:11:22 +0000 (14:11 -0500)]
Further refactoring in preparation for CONST_INTEGER (#8687)

Miscellaneous refactorings from trying to enable CONST_INTEGER.

2 years agoFix tuple printing in LFSC (#8696)
Andrew Reynolds [Mon, 2 May 2022 00:32:32 +0000 (19:32 -0500)]
Fix tuple printing in LFSC (#8696)

We weren't collecting them as user-defined types after the recent refactor to Tuples.

2 years agoProperly represent Tuples in the TypeNode AST (#8648)
Andrew Reynolds [Fri, 29 Apr 2022 21:49:13 +0000 (16:49 -0500)]
Properly represent Tuples in the TypeNode AST (#8648)

This makes it so that Tuple types are properly represented in the AST. It also removes a spurious restriction that disallowed higher-order tuples (this was leftover from a very old sanity check in the old API).

For example, a tuple type over (Int, Int) is now (TUPLE_TYPE INT INT) instead of a DATATYPE_TYPE constant.

Tuple types behave exactly like datatypes; we can still retrieve their DType as before.

This is in preparation for gradual types and symbolic tuple projections.

2 years agoAdd simple type rule for real-or-int arguments (#8685)
Andres Noetzli [Fri, 29 Apr 2022 20:49:21 +0000 (13:49 -0700)]
Add simple type rule for real-or-int arguments (#8685)

This adds a simple type rule, ARealOrInteger, which checks whether the
argument of an operator is either a Real or and Int. Note that this
is currently equivalent to AReal, but the plan is to make AReal
strict in the future.

2 years agoReplace mkConst(CONST_RATIONAL) by mkConstReal (#8686)
Gereon Kremer [Fri, 29 Apr 2022 20:30:07 +0000 (13:30 -0700)]
Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686)

This PR removes the usages of CONST_RATIONAL in the nonlinear arithmetic solver.

2 years agoTowards proper usage of TO_REAL (#8680)
Andrew Reynolds [Fri, 29 Apr 2022 19:35:04 +0000 (14:35 -0500)]
Towards proper usage of TO_REAL (#8680)

This is work towards making the rewriter preserve types, which is work towards eliminating subtyping.

This makes it so that the arithmetic rewriter does not simply drop TO_REAL from all terms, as this may change the type of the Node. Instead, TO_REAL is pulled upwards, and can be removed beneath arithmetic relations. TO_REAL is not eliminated if it occurs as a child of an operator not belonging to arithmetic. For example if x,y : Int:

(= (+ (to_real x) y) 0.0) ---> (= (to_real (+ x y)) 0.0) ---> (= (+ x y) 0.0) ; note this is the same rewritten form as before
(P (+ (to_real x) y)) ---> (P (to_real (+ x y))).

The one exception is that to_real applied to constants is simply dropped (for now), for example:

(to_real 5) ---> 5

where above, a Real term is rewritten to an Int term. (Fixing this will require further PRs that make integer constants of kind CONST_INTEGER and integral CONST_RATIONAL have Real type, thus we can have the above rewrite return 5 that is constant and has type Real).

Several quantifiers utilities are patched to preserve their behavior wrt handling TO_REAL.

Finally, a few fixes for subtypes are made to the regressions that we were not catching as errors before, and adds one regression.

The net effect of this PR is that the rewritten form of terms may have to_real applications that occur as direct children of symbols from other theories. Special care is required for preregistration, shared terms, and getting model values in the linear solver to strip off TO_REAL if necessary before using the (unmodified) interface to the linear solver.

FYI @barrettcw

2 years agoDocument non-standard string operators (#8679)
Andres Noetzli [Fri, 29 Apr 2022 18:45:21 +0000 (11:45 -0700)]
Document non-standard string operators (#8679)

This adds documentation for `str.indexof_re`, `str.update`, `str.rev`,
`str.to_lower`, and `str.to_upper`. Note that it moves the documentation
of strings to the "non-standard or extended theories".

2 years agoEnsure mkConstInt is used on integral rationals only (#8683)
Andrew Reynolds [Fri, 29 Apr 2022 17:49:05 +0000 (12:49 -0500)]
Ensure mkConstInt is used on integral rationals only (#8683)

This is work towards using CONST_INTEGER for integer constants.

This corrects a few places that incorrectly assumed that integers were necessary.

2 years agoRefactor interfaces for E-matching (#8665)
Andrew Reynolds [Fri, 29 Apr 2022 15:43:55 +0000 (10:43 -0500)]
Refactor interfaces for E-matching (#8665)

InstMatch objects are now fully owned by Triggers. They are passed by reference to InstMatchGenerators.

This also simplifies the interfaces by not passing the quantified formulas.

This is in preparation for making InstMatch objects carry entailment test information.

2 years agoMake extended rewriter use standard Subs utility (#8682)
Andrew Reynolds [Fri, 29 Apr 2022 15:22:20 +0000 (10:22 -0500)]
Make extended rewriter use standard Subs utility (#8682)

This is work towards ensuring all substitutions are strictly typed.

2 years agoAdd an option to enable all testers. (#8676)
Abdalrhman Mohamed [Fri, 29 Apr 2022 03:58:16 +0000 (22:58 -0500)]
Add an option to enable all testers. (#8676)

2 years agoAdd missing parenthesis for bags documentation (#8673)
yoni206 [Fri, 29 Apr 2022 03:38:35 +0000 (06:38 +0300)]
Add missing parenthesis for bags documentation (#8673)

2 years agoAdd unit test for code not exposed by java API (#8678)
Gereon Kremer [Fri, 29 Apr 2022 03:21:12 +0000 (20:21 -0700)]
Add unit test for code not exposed by java API (#8678)

This PR adds a C++ unit test that explicitly calls into API functions that are not exposed by the java API. This fixes the issue of false positives in our API coverage checks, as some parts of the C++ API are legitimately not used by the java API.
It also corrects a few other minor issues.

2 years agoAdd unit test for code not exposed by python API (#8677)
Gereon Kremer [Fri, 29 Apr 2022 01:09:03 +0000 (18:09 -0700)]
Add unit test for code not exposed by python API (#8677)

This PR adds a C++ unit test that explicitly calls into API functions that are not exposed by the python API. This fixes the issue of false positives in our API coverage checks, as some parts of the C++ API are legitimately not used by the python API.

2 years agoAdd some missing API tests (#8669)
Gereon Kremer [Fri, 29 Apr 2022 00:47:10 +0000 (17:47 -0700)]
Add some missing API tests (#8669)

This PR adds a couple of simple API tests for parts of the API that are not covered yet.

2 years agoMove tests around (#8670)
Gereon Kremer [Thu, 28 Apr 2022 18:30:46 +0000 (11:30 -0700)]
Move tests around (#8670)

This PR moves two tests that dealt with particular issues out of unit/api/cpp (which should only have generic unit tests). They are now in unit/theory and api/cpp/.

2 years agoint-blaster: not allowing higher order functions (#8674)
yoni206 [Thu, 28 Apr 2022 17:08:43 +0000 (20:08 +0300)]
int-blaster: not allowing higher order functions (#8674)

Currently we throw an OptionException if higher order logic is enabled, but we only check this once we reach an APPLY_FUN node.
This PR does the check regardless of APPLY_FUN, thus capturing, e.g. BAG_MAP.
Fixes cvc5/cvc5-projects#415.
The PR also includes a simplified version of the test from that issue.

2 years agoMove datatype split inference scheme to its own method (#8664)
Andrew Reynolds [Thu, 28 Apr 2022 16:38:28 +0000 (11:38 -0500)]
Move datatype split inference scheme to its own method (#8664)

2 years agoClean code for datatypes split (#8667)
Andrew Reynolds [Thu, 28 Apr 2022 13:42:58 +0000 (08:42 -0500)]
Clean code for datatypes split (#8667)

Non-moving version of #8664.

2 years agoMake labelled separation logic asserts preserve labels (#8671)
Andrew Reynolds [Thu, 28 Apr 2022 12:27:32 +0000 (07:27 -0500)]
Make labelled separation logic asserts preserve labels (#8671)

This is a first step towards fixing #8659.

The issue is that when two labels are equal, we assume they refer to subheaps of the same heap. This is incorrect for magic wand. This ensures we preserve labels, a further PR will ensure that syntactic equality on labels (instead of semantic equality) is used for knowing when two pto constraints must be unified. This means that SEP_LABEL nodes should never be rewritten.

2 years agoFix PyUnicode_AsWideCharString signature (#8522)
Andrey Andreyevich Bienkowski [Thu, 28 Apr 2022 01:22:03 +0000 (01:22 +0000)]
Fix PyUnicode_AsWideCharString signature (#8522)

Add proper exception specification to the `PyUnicode_AsWideCharString` signature.

2 years agoAdd resource limiting to coverings solver (#8672)
Gereon Kremer [Thu, 28 Apr 2022 00:51:20 +0000 (17:51 -0700)]
Add resource limiting to coverings solver (#8672)

Right now, resource limits are not checked while the coverings solver is computing. This PR adds a new resource and spends it within every recursive call of the coverings solver. This fixes cases where cvc5 does not honor the per-call time limit on QF_NRA.

2 years agoAdd option to apply constant propagation for all learned literals (#8668)
Andrew Reynolds [Wed, 27 Apr 2022 19:12:07 +0000 (14:12 -0500)]
Add option to apply constant propagation for all learned literals (#8668)

Adds `--simplification-bcp`, disabled by default.

2 years agoRefactoring of initial lemmas in datatypes (#8666)
Andrew Reynolds [Wed, 27 Apr 2022 13:25:36 +0000 (08:25 -0500)]
Refactoring of initial lemmas in datatypes (#8666)

This is work towards revising how/when the datatypes instantiate rule is applied.

This simplifies the management of when new terms are registered in the theory of datatypes.

We now use the equality engine's eqNotifyNewClass callback to know when a term should be considered. Previously, this was split over two methods (additionally, collectTerms).

Most importantly, this eliminates the need for a manual addition of the "instantiated constructor term" in getInstantiateCons, which complicates the logic for the impact of applying the datatypes instantiate rule.

2 years agoMinor improvements for entailment test (#8663)
Andrew Reynolds [Wed, 27 Apr 2022 00:01:39 +0000 (19:01 -0500)]
Minor improvements for entailment test (#8663)

Makes some minor improvements to the existing (non-incremental) entailment tests, based on comparing with a new implementation.

2 years agoMinor improvements to quantifiers utilities (#8661)
Andrew Reynolds [Tue, 26 Apr 2022 23:38:14 +0000 (18:38 -0500)]
Minor improvements to quantifiers utilities (#8661)

2 years agoMake IndexTrie take nodes (#8649)
Andrew Reynolds [Tue, 26 Apr 2022 22:37:37 +0000 (17:37 -0500)]
Make IndexTrie take nodes (#8649)

This makes the class easier to use and allows for a usage where the null node is interpreted as specifying all nodes.

This is in preparation for using this class for testing whether an instantiation from any instantiation strategy is currently feasible based on learning in the style of fail masks from Janota et al FMCAD 2021.

Also, this class should be renamed to something more appropriate, since it no longer takes indices.

FYI @MikolasJanota

2 years agoMove rep set iterator to its own file (#8647)
Andrew Reynolds [Tue, 26 Apr 2022 22:06:45 +0000 (17:06 -0500)]
Move rep set iterator to its own file (#8647)

2 years agoRefactor InstMatch (#8646)
Andrew Reynolds [Tue, 26 Apr 2022 21:43:27 +0000 (16:43 -0500)]
Refactor InstMatch (#8646)

Also simplifies the (old) version of multi trigger matching, which copied InstMatch objects unnecessarily, and also used EqualityEngine iteration instead of iterating on a trie.

This is in preparation for making InstMatch objects optionally track fast (and generalized) failures based on configurable criteria.

2 years agoRefactor mkRep option for instantiation (#8657)
Andrew Reynolds [Tue, 26 Apr 2022 19:56:40 +0000 (14:56 -0500)]
Refactor mkRep option for instantiation (#8657)

This removes mkRep as an option for addInstantiation.

It adds a new interface for making term vectors representative, which is required for FMF instantiation.

2 years agoAdd some missing resultants in the coverings solver (#8662)
Gereon Kremer [Tue, 26 Apr 2022 17:17:23 +0000 (10:17 -0700)]
Add some missing resultants in the coverings solver (#8662)

This PR fixes a subtle corner case in the generalization within the coverings solver. When generalizing a single interval that spans the whole real line (i.e. from -infty to infty) that is based on multiple polynomials (most likely because the origin constraint factored) we did not include their pairwise resultants.
This detail is arguably missing in the paper, or rather hidden in a very vague notion of "performing standard CAD simplifications".
Fixes #8638.

2 years agoSimplify internal represenation of uninterpreted sorts (#8660)
Andrew Reynolds [Tue, 26 Apr 2022 15:45:45 +0000 (10:45 -0500)]
Simplify internal represenation of uninterpreted sorts (#8660)

2 years agoFix GMP cross-compilation when Wine installed (#8645)
Andres Noetzli [Tue, 26 Apr 2022 02:06:19 +0000 (19:06 -0700)]
Fix GMP cross-compilation when Wine installed (#8645)

When Wine is installed on the system, our current invocation of GMP's
`configure` fails. To fix the issue, we pass `CC_FOR_BUILD` that is used
to compile build-time programs. When compiling GMP with `--enable-cxx`,
it also seems to be necessary to pass `--build` to make `configure`
pass. Passing `--build` for cross-compilation builds is also recommended
by the [GMP documentation](https://gmplib.org/manual/Build-Options).

2 years agoSimplify internal representation of instantiated sorts (#8620)
Andrew Reynolds [Tue, 26 Apr 2022 01:16:55 +0000 (20:16 -0500)]
Simplify internal representation of instantiated sorts (#8620)

Previously, sort constructors were stored as underlying operator of the NodeValue of instantiated sorts. This made it very difficult to access what sort constructor was used to construct the uninterpreted sort. Moreover, this representation made it virtually impossible to have a clean implementation of the LFSC printer for instantiated uninterpreted sorts, which requires renaming sort constructors.

This introduces a new kind INSTANTIATED_SORT_TYPE, which acts as an uninterpreted sort. The sort constructor is stored as the first child in its AST, which is analogous to parametric datatypes. It furthermore restricts SORT_TYPE to 0 children.

This is work towards having correct LFSC proof output when the input contains instantiated uninterpreted sorts.

2 years ago[Regressions] Use Wine for Windows builds (#8652)
Andres Noetzli [Mon, 25 Apr 2022 21:50:14 +0000 (14:50 -0700)]
[Regressions] Use Wine for Windows builds (#8652)

This changes our build system to use Wine when we are testing a
cross-compiled Windows build. It updates the post-processing in the
regression script to remove `\r` characters and updates two regressions
to make them compatible with Windows builds.

2 years agoMove VTS term cache to term registry (#8656)
Andrew Reynolds [Mon, 25 Apr 2022 20:07:51 +0000 (15:07 -0500)]
Move VTS term cache to term registry (#8656)

This is in preparation for simplifying the interface to Instantiate::addInstantiation, where the VTS cache can be consulted to ask if VTS is necessary.

2 years agoOption exception for quantified bit-vectors + eager bitblasting + incremental (#8658)
Andrew Reynolds [Mon, 25 Apr 2022 19:00:51 +0000 (14:00 -0500)]
Option exception for quantified bit-vectors + eager bitblasting + incremental (#8658)

Fixes #8654.

2 years agoMake BVInstantiatorUtil an EnvObj (#8633)
Andrew Reynolds [Mon, 25 Apr 2022 18:21:57 +0000 (13:21 -0500)]
Make BVInstantiatorUtil an EnvObj (#8633)

Eliminates 5 of the remaining 8 static calls to Rewriter::rewrite.

2 years agoAdd custom targets for specific testers. (#8653)
Abdalrhman Mohamed [Mon, 25 Apr 2022 16:08:23 +0000 (11:08 -0500)]
Add custom targets for specific testers. (#8653)

This adds custom targets to run a specific tester (e.g., `regress-lfsc`).

Signed-off-by: Abdalrhman M Mohamed <abdalrhman-mohamed@uiowa.edu>
2 years agoMinor cleanup of NodeManager (#8650)
Andrew Reynolds [Sat, 23 Apr 2022 15:48:28 +0000 (10:48 -0500)]
Minor cleanup of NodeManager (#8650)

2 years agoAdd `deep-restart` option (#8644)
Andrew Reynolds [Fri, 22 Apr 2022 20:03:33 +0000 (15:03 -0500)]
Add `deep-restart` option (#8644)

Adds the ability to have the SmtSolver automatically deep restart after a criteria is met (we have learned new top-level literals, and a threshold of time since the last learned literal has passed). This can be used for non-incremental satisfiability queries only.

By default, --deep-restart=input kicks in on 155 of our regressions, this adds 4 delta-debugged regressions that exercise the feature.

2 years agoAdd tester for LFSC printer. (#8606)
Abdalrhman Mohamed [Thu, 21 Apr 2022 06:45:04 +0000 (01:45 -0500)]
Add tester for LFSC printer. (#8606)

This adds an option to check the LFSC proofs generated by `cvc5` for unsat benchmarks. This does not enable the tester in CI as it fails for many benchmarks.

2 years ago[Seq] Remove `SkolemCache::mkSkolemSeqNth()` (#8643)
Andres Noetzli [Thu, 21 Apr 2022 05:28:52 +0000 (22:28 -0700)]
[Seq] Remove `SkolemCache::mkSkolemSeqNth()` (#8643)

This removes the `SkolemCache::mkSkolemSeqNth()` method. Instead of
handling the out-of-bounds case with a UF, we just use `seq.nth` in its
original form for the out-of-bounds case (and rely on the fact that the
equality engine is configured to perform congruence closure on that
kind). This is part of the changes for the paper on sequences.

2 years agoAdd bag.partition evaluation (#8637)
mudathirmahgoub [Thu, 21 Apr 2022 04:46:43 +0000 (23:46 -0500)]
Add bag.partition evaluation (#8637)

2 years agoAdd utilities in preparation for deep restarts (#8642)
Andrew Reynolds [Wed, 20 Apr 2022 22:59:35 +0000 (17:59 -0500)]
Add utilities in preparation for deep restarts (#8642)

2 years agoRemove unused `SEQ_NTH_TOTAL` kind (#8048)
Andres Noetzli [Wed, 20 Apr 2022 21:44:01 +0000 (14:44 -0700)]
Remove unused `SEQ_NTH_TOTAL` kind (#8048)

Originally, the idea was to expand the definition of `SEQ_NTH` to use
`SEQ_NTH_TOTAL` (i.e., a total version of that operator), but we have
since then decided to just use `SEQ_NTH`.

2 years agoImprove handling of `(push)` and `(pop)` (#8641)
Andres Noetzli [Wed, 20 Apr 2022 21:00:31 +0000 (14:00 -0700)]
Improve handling of `(push)` and `(pop)` (#8641)

This extends PushCommand and PopCommand to take a number of levels
to push/pop. We have support for pushing an arbitrary number of levels
at the API level, so this simplifies the parser code and makes dumping
more precise (previously, we were dumping (push 2) as two (push 1)
commands).

2 years agoAdd declare-oracle-fun command (#8621)
Andrew Reynolds [Wed, 20 Apr 2022 20:04:21 +0000 (15:04 -0500)]
Add declare-oracle-fun command (#8621)

In preparation for adding declare-oracle-fun to the API/parser.

2 years agoMinor simplifications for datatype selector triggers (#8636)
Andrew Reynolds [Wed, 20 Apr 2022 19:41:34 +0000 (14:41 -0500)]
Minor simplifications for datatype selector triggers (#8636)

This is leftover simplification from the fact that (s x) is no longer expanded to (ite (is-C x) (s_total x) (uf x)).

2 years agoint-blaster: direct support for bvcomp (#8640)
yoni206 [Wed, 20 Apr 2022 15:39:16 +0000 (18:39 +0300)]
int-blaster: direct support for bvcomp (#8640)

This PR adds a translation of bvcomp using an ite.
Fixes cvc5/cvc5-projects#417
and contains the failed formula as a regression.

2 years agoRemove redundant assertion in int-blaster (#8639)
yoni206 [Wed, 20 Apr 2022 14:48:31 +0000 (17:48 +0300)]
Remove redundant assertion in int-blaster (#8639)

When translating nodes with no children, the default case does not change the original node, and so we do not need to assume anything about the node. fixes cvc5/cvc5-projects#416 . The example from the issue is added as a unit test.

2 years agoUpdates to zero level learner (#8597)
Andrew Reynolds [Wed, 20 Apr 2022 01:36:51 +0000 (20:36 -0500)]
Updates to zero level learner (#8597)

Now tracks learned literals for all types.  Unifies the output of `-o learned-literals`.

Followup PRs will add the deep restart feature, which configures which kind of learned literals can be used when restarting.

2 years agoAvoid trivial equalities in explanation of SETS_CARD_CYCLE (#8635)
Andrew Reynolds [Tue, 19 Apr 2022 20:36:54 +0000 (15:36 -0500)]
Avoid trivial equalities in explanation of SETS_CARD_CYCLE (#8635)

This was the root cause of cvc5/cvc5-projects#178.

2 years agoSimplify implementation of subtype methods in TypeNode (#8634)
Andrew Reynolds [Tue, 19 Apr 2022 19:35:40 +0000 (14:35 -0500)]
Simplify implementation of subtype methods in TypeNode (#8634)

Also deletes unused data that was used for an inference schema involving subtypes in sets.

2 years agoAdd table.project evaluator (#8632)
mudathirmahgoub [Tue, 19 Apr 2022 18:49:14 +0000 (13:49 -0500)]
Add table.project evaluator (#8632)

This PR

adds evaluator for table.project operator
updates the parser to interpret "Table" as a table with zero columns

2 years agoMove linear arithmetic solver to theory::arith::linear (#8628)
Andrew Reynolds [Tue, 19 Apr 2022 18:05:12 +0000 (13:05 -0500)]
Move linear arithmetic solver to theory::arith::linear (#8628)

This moves the current linear arithmetic solver to src/theory/arith/linear, and inside `cvc5::internal::theory::arith::linear`.

Some code uses internal utilities from `arith::linear`, although this should be minimized.

This is preparation for breaking dependencies with the old code.

2 years agoGeneralize concat conflict for sequences in LFSC (#8625)
Andrew Reynolds [Tue, 19 Apr 2022 17:15:33 +0000 (12:15 -0500)]
Generalize concat conflict for sequences in LFSC (#8625)

This ensures LFSC proofs are correct when using CONCAT_CONFLICT for sequences.

In detail, to justify why (seq.++ (seq.unit c1) t1) = (seq.++ (seq.unit c2) t2) is a conflict, where c1 and c2 are constants, we require an explicit step to evalute (seq.unit c1) = (seq.unit c2) to false, since c1 and c2 are theory-specific constants.

Note this is different from (str.++ (char n1) t1) = (str.++ (char n2) t2) where a syntactic check of n1 and n2 suffices.

This fixes proof checking for regress0/seq/seq-types.smt2.

2 years agoRemove instances of `check-proofs` in regressions. (#8630)
Abdalrhman Mohamed [Mon, 18 Apr 2022 22:21:22 +0000 (17:21 -0500)]
Remove instances of `check-proofs` in regressions. (#8630)

This PR removes usages of check-proofs option according to the following rules:

unsat and no-check-proofs --> DISABLE-TESTER: proof
unsat and check-proofs --> remove option
sat and no-check-proofs --> remove option
sat and check-proofs --> change to produce-proofs
no-produce-proofs --> DISABLE-TESTER: proof

2 years agoAdd some missing FP symbols to LFSC (#8629)
Andrew Reynolds [Mon, 18 Apr 2022 22:01:34 +0000 (17:01 -0500)]
Add some missing FP symbols to LFSC (#8629)

2 years agoDistinguish name variants for types in LFSC node converter (#8624)
Andrew Reynolds [Mon, 18 Apr 2022 21:29:24 +0000 (16:29 -0500)]
Distinguish name variants for types in LFSC node converter (#8624)

This PR ensures we distinguish names for cases where types and terms are given the same name.

In particular, this generalizes the getNameForUserNameOf to work with node identifiers instead of Node, so that TypeNode can also use this method for assigning unique names.

It also adds preliminary support for uninterpreted sort constructors in the LFSC node converter.

This fixes 4 more LFSC failures on our regressions.

2 years agoMake more utilities distinguish Int and Real (#8626)
Andrew Reynolds [Mon, 18 Apr 2022 17:56:29 +0000 (12:56 -0500)]
Make more utilities distinguish Int and Real (#8626)

Towards eliminating arithmetic subtyping.

2 years agoSimplify management of separation logic heap (#8580)
Andrew Reynolds [Mon, 18 Apr 2022 13:58:05 +0000 (08:58 -0500)]
Simplify management of separation logic heap (#8580)

The separation logic heap is conceptually an extension of the logic, which lives in Env. This PR moves the separation logic heap types from TheoryEngine to Env.

It furthermore makes it so that declaring the separation logic heap does not force initialization of the SolverEngine, meaning that further declarations/options may be done after setting the heap.

This is in preparation for making the SmtSolver class easier to deep reset.

2 years agoRemove support for unused `declare-*` commands (#8623)
Andres Noetzli [Mon, 18 Apr 2022 13:30:30 +0000 (06:30 -0700)]
Remove support for unused `declare-*` commands (#8623)

This commit removes support for
declare-sorts/declare-funs/declare-preds. These commands seem to
be a leftover of an earlier SMT-LIB draft [0]. We only had a test for
declare-funs and Z3 doesn't support declare-funs either.

[0] http://homepage.cs.uiowa.edu/~astump/papers/smt-cmd-lang.pdf

2 years agoFix internal type issue for congruence over quantifiers in LFSC post-processor (...
Andrew Reynolds [Thu, 14 Apr 2022 23:25:09 +0000 (18:25 -0500)]
Fix internal type issue for congruence over quantifiers in LFSC post-processor (#8619)

Avoids debug assertions in LFSC proof conversion when doing congruence over closures.

2 years agoImplement internal support for (definitional) satisfiability modulo oracles (#8618)
Andrew Reynolds [Thu, 14 Apr 2022 22:53:28 +0000 (17:53 -0500)]
Implement internal support for (definitional) satisfiability modulo oracles (#8618)

Adds implementation of OracleEngine, which adds lemmas of the form (= (f c) d) on demand for I/O pairs (c,d) from oracle calls.

2 years agoMake LFSC printer robust to internal types (#8616)
Andrew Reynolds [Thu, 14 Apr 2022 21:13:04 +0000 (16:13 -0500)]
Make LFSC printer robust to internal types (#8616)

This makes the LFSC node converter track the "user declared" symbols and types that it encounters.

It furthermore makes the "dry run" phase of proof printing happen before types and symbols are declared, so that all declared symbols are found before the preamble of LFSC proofs are printed.

These changes are specifically to fix cases where a internal type is generated that does not appear in the input. For example, some preprocessing passes may construct auxiliary uninterpreted sorts.

This fixes 6 more LFSC failures from our regressions.

2 years agoImplement internal support for synthesis modulo oracles (#8617)
Andrew Reynolds [Thu, 14 Apr 2022 19:48:23 +0000 (14:48 -0500)]
Implement internal support for synthesis modulo oracles (#8617)

SyMO is implemented as a preprocessor for SMT queries in the verification subsolver of SyGuS.

2 years agoRemove static calls to rewrite involving array constants (#8613)
Andrew Reynolds [Thu, 14 Apr 2022 19:11:57 +0000 (14:11 -0500)]
Remove static calls to rewrite involving array constants (#8613)

The type enumerators for arrays and functions relied on static calls to the rewriter. This is overkill, as the appropriate calls to the utility method normalizeConstant in the array rewriter class suffices.

The eliminates 2 of the remaining static calls to the rewriter.

2 years agoImprovements to phase shifting + purification lemmas (#8598)
Andrew Reynolds [Thu, 14 Apr 2022 18:00:30 +0000 (13:00 -0500)]
Improvements to phase shifting + purification lemmas (#8598)

Makes 3 improvements to phase shifting + purification lemmas:
(1) we use purification skolems when possible, e.g. for exp(t), or sin(c) where -pi <= c <= pi, since it is unnecessary to assert c is in proper phase. This also adds proofs for purification of exp, which is hence trivial.
(2) we make the phase shift variable a real for which is_int holds. This avoids mixed int/real arithmetic, in preparation for eliminating subtyping
(3) the proof checker and sine solver use a common utility for getting the phase shift lemma.

2 years agoRevised partitioning (#8143)
Amalee Wilson [Thu, 14 Apr 2022 15:26:49 +0000 (08:26 -0700)]
Revised partitioning (#8143)

This adds the "revised" partitioning algorithm to the splitter and adds support for collecting literals from the sat solver. There is only one partitioning strategy in this PR, but the others will be added in subsequent PRs.

2 years ago[proofs] [dot] New way to traverse the proof when printing a .dot DAG (#8610)
vinciusb [Thu, 14 Apr 2022 14:00:38 +0000 (11:00 -0300)]
[proofs] [dot] New way to traverse the proof when printing a .dot DAG (#8610)

Change the way cvc5 traverse and print the proof when --proof-dot-dag option is used. The main change is related to the way the printer tracks visited proof nodes. The new conditions are:

- If the proof node has already been visited inside the current scope.
- If the proof node is closed (i.e. does not contains a subproof whose rule is ASSUME) and has already been visited (here the condition is global and the scope doesn't matter).

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com
2 years agoIntegrate oracle checker into quantifiers term registry (#8604)
Andrew Reynolds [Thu, 14 Apr 2022 13:36:38 +0000 (08:36 -0500)]
Integrate oracle checker into quantifiers term registry (#8604)

Also incorporates into sygus term database. For SyMO, oracle function symbols act analogously to recursive function definitions; the oracle checker is used to rewrite terms in the same contexts as when recursive function definitions are evaluated.

2 years agoFix spurious assertion involving subtypes (#8611)
Andrew Reynolds [Thu, 14 Apr 2022 13:16:49 +0000 (08:16 -0500)]
Fix spurious assertion involving subtypes (#8611)

Fixes #8609.

2 years agoUpdate LFSC version (#8614)
Andrew Reynolds [Thu, 14 Apr 2022 04:46:19 +0000 (23:46 -0500)]
Update LFSC version (#8614)

Now has a different expected output ("success" for each check).

2 years agoAdd Relation and Table types to SMTLib parser (#8605)
mudathirmahgoub [Wed, 13 Apr 2022 18:54:27 +0000 (13:54 -0500)]
Add Relation and Table types to SMTLib parser (#8605)

2 years agoFix type issue for FP constants in LFSC node converter (#8612)
Andrew Reynolds [Wed, 13 Apr 2022 14:56:43 +0000 (09:56 -0500)]
Fix type issue for FP constants in LFSC node converter (#8612)

Fixes type errors in debug builds.

2 years agoFix spurious assertion failure caused by subtyping in LFSC proof postprocessor (...
Andrew Reynolds [Tue, 12 Apr 2022 22:35:05 +0000 (17:35 -0500)]
Fix spurious assertion failure caused by subtyping in LFSC proof postprocessor (#8608)

Also removes an old case for parametric datatypes in getBaseType, which is incorrect since datatypes not longer use subtyping.

This avoids more assertion failures in debug mode for LFSC due to subtypes.

2 years agoFix type issue for LFSC null terminator (#8607)
Andrew Reynolds [Tue, 12 Apr 2022 21:54:25 +0000 (16:54 -0500)]
Fix type issue for LFSC null terminator (#8607)

This fixes an assertion failure when producing LFSC proofs in debug mode.

The issue currently does not impact the correctness of the code, although this will be important if subtypes are eliminated.

2 years agoAdd oracle checker utility (#8603)
Andrew Reynolds [Tue, 12 Apr 2022 18:55:05 +0000 (13:55 -0500)]
Add oracle checker utility (#8603)

This is a utility that allocates oracle callers for oracle functions on demand and can be used to convert a term containing oracle function symbols into its evaluated form.

It will be used for both SMTO (for checking consistency of oracle interfaces) and SyMO (as part of refinement lemma evaluation in CEGIS).

2 years agoAdd oracle caller utility (#8599)
Andrew Reynolds [Tue, 12 Apr 2022 14:59:14 +0000 (09:59 -0500)]
Add oracle caller utility (#8599)

The implementation of this class has a placeholder for calling external binaries, which will be filled in a later PR.

2 years agoMaking some benchmarks SMT-LIB compliant for subtypes (#8600)
Andrew Reynolds [Tue, 12 Apr 2022 14:19:53 +0000 (09:19 -0500)]
Making some benchmarks SMT-LIB compliant for subtypes (#8600)

This makes some of our regressions compliant for arithmetic subtyping. This is required to make these benchmarks parsable when subtyping is eliminated.

We should discuss whether we should be permissive for such benchmarks. Regardless, the majority of our regressions should be SMT-LIB compliant.

2 years agoFix more misuses of arithmetic subtypes (#8601)
Andrew Reynolds [Tue, 12 Apr 2022 13:58:18 +0000 (08:58 -0500)]
Fix more misuses of arithmetic subtypes (#8601)

2 years ago[proofs] [dot] Print nodes clusters at dot format (#8574)
vinciusb [Tue, 12 Apr 2022 13:13:56 +0000 (10:13 -0300)]
[proofs] [dot] Print nodes clusters at dot format (#8574)

Add a printer option that allows the dot printer to identify each node type and group them up in node clusters. These cluster are determined according to "part of the proof" whether a node belongs to:

- input
- sat proof
- cnf proof
- theory lemma proof
- preprocessing

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com
2 years agoMore cleaning uses of arithmetic subtyping (#8595)
Andrew Reynolds [Mon, 11 Apr 2022 22:13:46 +0000 (17:13 -0500)]
More cleaning uses of arithmetic subtyping (#8595)

Towards eliminating arithmetic subtyping.

2 years agoAdd oracle engine to quantifiers engine (#8589)
Andrew Reynolds [Mon, 11 Apr 2022 21:06:10 +0000 (16:06 -0500)]
Add oracle engine to quantifiers engine (#8589)

This class is the subsolver of quantifiers engine for handling oracles in SMTO. The implementation of this class will be added in followup PRs.

It also contains a utility method for constructing oracle interfaces.

2 years agoRemove spurious case of ppRewrite (#8596)
Andrew Reynolds [Mon, 11 Apr 2022 15:33:54 +0000 (10:33 -0500)]
Remove spurious case of ppRewrite (#8596)

Constants equal to constants are always rewritten to false.

2 years agoAdd learned literal type and prop learned database (#8582)
Andrew Reynolds [Mon, 11 Apr 2022 14:10:44 +0000 (09:10 -0500)]
Add learned literal type and prop learned database (#8582)

In preparation for deep restart feature, and for extending the get-learned-literal interface to multiple types.

2 years agoSimplify parser (#8592)
Andres Noetzli [Fri, 8 Apr 2022 22:00:23 +0000 (15:00 -0700)]
Simplify parser (#8592)

This commit simplifies our parser by removing code that is not relevant
anymore since the removal of support for SMT-LIB <=2.6.

2 years agoMinor refactoring of smt2 printer (#8588)
Andrew Reynolds [Fri, 8 Apr 2022 21:37:09 +0000 (16:37 -0500)]
Minor refactoring of smt2 printer (#8588)

2 years agoDo not allow unresolved sorts in smt2 (#8587)
Andrew Reynolds [Fri, 8 Apr 2022 21:17:29 +0000 (16:17 -0500)]
Do not allow unresolved sorts in smt2 (#8587)

This simplifies the smt2 parser so that we never parse "inlined" unresolved sorts. This infrastructure was used for accomodating the ad-hoc datatype syntax from SMT-LIB <=2.5, and SyGuS 1.0.

We now assume that sorts are fully declared wherever we parse them.

2 years agoEliminate more uses of CONST_RATIONAL (#8590)
Andrew Reynolds [Fri, 8 Apr 2022 20:58:02 +0000 (15:58 -0500)]
Eliminate more uses of CONST_RATIONAL (#8590)

To eliminate arithmetic subtyping, we require distinguishing CONST_RATIONAL and CONST_INTEGER internally. Code should avoid usage of these kinds and use trusted utilities instead (e.g. mkConstReal, mkConstInst, isConst).

2 years agoProperly parse numerals as real when integers are disabled (#8591)
Andrew Reynolds [Fri, 8 Apr 2022 20:38:52 +0000 (15:38 -0500)]
Properly parse numerals as real when integers are disabled (#8591)

SMT-LIB says numerals are real when integers are not included in the logic.

Due to subtyping, we don't complain internally, although if subtyping is eliminated, this fix is necessary.

2 years agoGeneralization for sygus verify utility (#8586)
Andrew Reynolds [Thu, 7 Apr 2022 22:14:08 +0000 (17:14 -0500)]
Generalization for sygus verify utility (#8586)

This is in preparation for synthesis modulo oracles (SyMO), where the verification loop may run multiple times for a given solution. In a follow up PR, the loop introduced in this PR may run multiple times when oracles are present, since oracle invocations in the subsolver may trigger further simplifications to the rewritten form of the specification.

It also makes it so that candidate models are generated for "unknown" results for subsolvers, which is required for SyMO.

2 years agoInternal representation of oracle interface quantifiers (#8585)
Andrew Reynolds [Thu, 7 Apr 2022 21:32:07 +0000 (16:32 -0500)]
Internal representation of oracle interface quantifiers (#8585)

This is the first step towards supporting SMT and synthesis modulo oracles.

It adds the kind required for specifying "oracle interface quantifiers", or, quantified formulas that specify constraints that depend on an external binary.

2 years agoAdd method to get leaves of a NodeTrie (#8583)
Andrew Reynolds [Thu, 7 Apr 2022 21:04:31 +0000 (16:04 -0500)]
Add method to get leaves of a NodeTrie (#8583)

From the oracles branch.

2 years agoMake sets and bags operators left-associative (#8584)
Andrew Reynolds [Thu, 7 Apr 2022 18:09:14 +0000 (13:09 -0500)]
Make sets and bags operators left-associative (#8584)

Makes it so that we parse n-ary applications of e.g. set.union in smt2.
Left associativity seems to be the case for difference operators in databases.
See
https://docs.microsoft.com/en-us/sql/t-sql/language-elements/set-operators-except-and-intersect-transact-sql?view=sql-server-ver15

2 years agoEliminate SmtSolver dependency on SolverEngineState (#8581)
Andrew Reynolds [Thu, 7 Apr 2022 13:07:39 +0000 (08:07 -0500)]
Eliminate SmtSolver dependency on SolverEngineState (#8581)

This is in preparation for making SmtSolver able to be deep reset (reconstructed) within in a SolverEngine instance.

2 years agoMinor fix for printing nullary operators in smt2 (#8577)
Andrew Reynolds [Thu, 7 Apr 2022 12:48:38 +0000 (07:48 -0500)]
Minor fix for printing nullary operators in smt2 (#8577)

2 years agoFix proof checker for SUBS (#8578)
Andrew Reynolds [Thu, 7 Apr 2022 12:29:53 +0000 (07:29 -0500)]
Fix proof checker for SUBS (#8578)

Could lead to proof checking failures when using `--proof-granularity=rewrite`