Conversation
mpreiner
reviewed
Apr 1, 2022
mpreiner
pushed a commit
to cvc5/cvc5
that referenced
this pull request
Apr 2, 2022
We are renaming files in the pythonic API to make it look less like it is somehow part of z3 (but still acknowledge that we took code from z3Py properly). This PR follows the change in cvc5/cvc5_pythonic_api#80.
mpreiner
pushed a commit
to mpreiner/cvc5
that referenced
this pull request
Apr 5, 2022
We are renaming files in the pythonic API to make it look less like it is somehow part of z3 (but still acknowledge that we took code from z3Py properly). This PR follows the change in cvc5/cvc5_pythonic_api#80.
adacore-bot
pushed a commit
to AdaCore/spark2014
that referenced
this pull request
May 23, 2022
* Update cvc5 from branch 'master'
to dde85f0d8c3d5a691f16e90db031dc84a22ab916
- Merging CVC5 main into AdaCore master
For V425-006
Change-Id: Ib27c06652b73355e7cb9e48104171ad80f3d59af
- bv: Add resource limits support for CaDiCaL. (#8788)
Fixes #8776.
- Simplification of smt2 printer for type ascriptions (#8801)
Previously had code for dealing with subtypes
- Move smt_util to preprocessing/util (#8799)
src/smt_util contains a single file that is only used by the miplib trick preprocessing pass. This moves it to preprocessing/util.
- Reenable assertion in skolem definition manager (#8797)
This reenables a variant of an assertion that was deleted in #8749, a weaker version of that assertion should now hold.
- Add option to send all instantiations in a bounded range (#8796)
There is a block of code in FMF instantiation that is questionable whether it is helpful, in particular for dealing with string reductions for long strings.
- Add cross-compilation for arm64 on macOS (#8758)
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
- More removing of unused code (#8806)
- Trying to break cycles when printing a .dot DAG (#8698)
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 deals with cycles between proof nodes that are in a ancestor/descendant relationship. The new conditions are:
- If any proof node under a first proof node has the hash equal to the first one, this would introduces a cycle. To avoid it, then no sharing between nodes happens in this case.
Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com
- New way to identify THEORY_LEMMA clusters when printing in the .dot format (#8745)
Change the way cvc5 identifies THEORY_LEMMA clusters when --print-dot-clusters option is used. Previously, only proof nodes with SCOPE rule after a CNF cluster could identify a THEORY_LEMMA cluster. Now, any of the following rules, after a CNF cluster, can identify it:
1. SCOPE
2. THEORY_LEMMA
3. Any rule R in the following range: CNF_ITE_NEG3 < R < LFSC_RULE
Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com
- Minor deleting of unused code (#8800)
Towards improving coverage.
- Add options and regressions to increase coverage (#8803)
Also corrects an issue with the text interface. When get-model is used with model cores, we do not currently filter the output. This ensures that we do.
- V516-002 update gitreview for new repo on master branch
Change-Id: I02ebacd96fc2998390aef1afcce21690ac62fdfa
- Basic cleanup of sep theory (#8790)
Most of the simplifications are due to the fact that we only handle a single heap type. (The solver was initially designed to potentially handle more than one heap type).
- Make skolem definition manager robust to definitions for already asserted skolems (#8749)
It makes the skolem definition manager more robust so that skolem definitions can be added for skolems that have already appeared in asserted literals. This was the initial motivation for the change in ordering. As a result, fixes #8347 and fixes cvc5/cvc5-projects#512. It also optimizes this class in a few ways.
It also comments more on the change to PropEngine introduced here: #8301 which led to performance degradation on a set of string benchmarks of interest.
- Eliminate subtypes (#8783)
- Refactor declare oracle command (#8742)
In preparation for adding oracle functions to API.
- Minor cleanup of datatypes theory (#8791)
- Fix LFSC proof construction for concat clash of sequences (#8739)
Changes the internal proof calculus to require an explicit disequality between character constants for clashing sequences.
Makes it so that the disequality is expanded prior to proof post-processing, so that character clashing is properly expanded as it may require rewriting.
- docs: Remove references to checkEntailed(). (#8789)
- Generalize pto constraint tracking for multiple heaps in sep theory (#8768)
Fixes #8659.
- Add getInterpolant with a grammar in the unit test for all language bindings (#8775)
Add getInterpolant with a grammar in the unit test for all language bindings
- new test for resolved issue (#8784)
#8412 is now fixed on main. This PR adds a regression from that issue.
closes #8412 .
- Last remaining fixes for eliminating subtyping (#8772)
Also fixes a debug failure for the nightlies.
This also changes mkTuple to not rely on subtyping (this method should regardless be deleted from our API, as it is not the recommended way of constructing tuples).
- [proofs] Generalize handling of constants merged in equality engine (#8781)
Previously the reconstruction of EUF proofs was not considering a corner case from the equality engine where it infers that two constants are disequal from other equalities, but these other equalities all become of the form x = x at the time we are explaining this disquality. In this case the constant disequality is justified with MERGED_THROUGH_CONSTANTS rather than MERGED_THROUGH_TRANS as other disequalities.
- Rename equality engine trace to print E-graph (#8780)
The current trace depends on `-t equality::internal`, which is pointless and
leads to confusion when one inevitably forgets this when checking which trace to
use to print the E-graph and the output does not contain it.
- Eliminate the use of CAST_TO_REAL (#8759)
This simplifies the implementation of the API by not relying on CAST_TO_REAL. This was used as a way of manually marking integral reals as having real type.
- Eliminate ops for parameterized type constructors (#8761)
We now preserve types when rewriting. This means that we no longer need to use operators that store the type of terms to construct in the cases of bags, sets, and sequences.
- Make arith substitute its own utility (#8765)
Arithmetic substitutions behave differently in two ways:
(1) they traverse only symbols belonging to arithmetic
(2) they allow mixing Int/Real
This makes ArithSubs derive from the more general Subs class with these two behavior changes.
This is one of the last remaining non-trivial steps towards for eliminating TypeNode::isSubtypeOf.
- Add heap-trail partitioning strategy, checks between partitions, and cubes with zero-level learned literals (#8703)
These changes extend the partition generator to be able to do the following:
Access the order_heap in MiniSat and make partitions from those literals.
Specify a number of checks between partitions. This is relevant for only the revised and strict-cube strategies.
Append zero-level learned literals to the partitions.
- Fixes and improvement for IAND solver (#8771)
This fixes a model soundness bug in the non-linear solver for IAND, which was caused by the core NL model solving for an IAND term. This adds 2 delta debugged variants of a benchmark from an application.
It also improves the value-based refinement scheme for IAND significantly by ensuring we take the modulus of model values. This should make it terminating.
- Eliminate use of getBaseType (#8764)
For the model, this was used for ensuring that we skipped enumerating the Real constant 1.0 if the Integer constant 1 already existed in the model. Now, these two nodes are disjoint, and due to #8740, the use of getBaseType in this context has no effect since the set of real and integer constants are disjoint.
It was also used in CEGQI in a similar manner, where since equivalence classes of Int and Real terms are disjoint, it is not necessary to search for e.g. Real variables in integer equivalence classes.
- Add utilities in preparation for supporting str.nth (#8766)
Work towards efficient support for to_lower/to_upper.
- Fix debug failures in LFSC proofs due to curried arithmetic operators (#8763)
This ensures we use different variants of PLUS, MULT, NONLINEAR_MULT internally to avoid type checking failures in debug mode during LFSC printing.
Fixes regression failures in debug mode for LFSC.
- Refactor logic exceptions during preregistration for arithmetic (#8769)
Fixes #8755.
- Update CoCoALib version (#8757)
This PR updates our cmake scripts for CoCoALib to use the latest and greatest version.
While we don't actually want to use any of the new features, the new version finally uses an Apache license!
- Minor refactoring for sep theory (#8753)
Work towards fixing #8659.
- Fix type of null terminator for ADD/MULT for LFSC (#8762)
This fixes many LFSC proof failures that are occurring now because of using 1.0 instead 1 as null terminator for MULT, and 0.0 instead of 0 for ADD.
- Eliminate use of subtypes from remainder of type rules (#8756)
This PR should be added before the minor release that advertises our policy change for subtyping.
- Preserve types in rewriter and make core type rules strict (#8740)
This is the key step for eliminating the use of subtyping.
This makes several changes:
(1) CONST_INTEGER is now used for integer constants, which is now exported in the API. The type rule for CONST_RATIONAL is changed to always return Real, even if its value is integral. This means we can distinguish real and integer versions of the integers. Note this also implies that the rewriter now fully preserves types, as rewriting TO_REAL applied to a constant integer will return a constant integral rational.
(2) The type rules for EQUAL, DISTINCT, ITE and APPLY_UF are made strict, in other words, we given a type exception for equalities between an Int and a Real. This restriction impacts the API.
(3) The arithmetic rewrite for (Real) equality casts integers to reals as needed to ensure Reals are only made equal to Reals. The net effect is that TO_REAL may appear on either side of equalities.
(4) The core arithmetic theory solver is modified in several places to be made robust to TO_REAL occurring as the top symbol of sides of equality.
Several assertions are strengthened or added to ensure that equalities and substitutions are between terms of the same type, when it is necessary to do so.
Two quantifiers regressions are modified since the solving techniques are not robust to TO_REAL. A few unit tests are fixed to use proper types.
- [docs] Marking internal comment in proofs docs (#8747)
- Make regular options access const (#8754)
One of the loose ends of the options refactor is that internal code can write to options at will, even when the accessing it via Env::getOptions() which returns a const reference. There are technical reasons for this, C++ does not propagate the constness into reference members.
This PR changes this behaviour by making the references members we use all over the place (options().smt.foo) const references and adding new functions writeSmt() which allow write access -- if you have a non-const handle to the options object.
In order to do that, this PR also changes all places that legitimately change the options (options handlers, set defaults, solver engine and places where we spawn subsolvers) to use the new syntax. After that, only a single place remains: the solver engine attempts to write the filename (from Solver::setInfo("filename", "...");) into the original options (that are restored to the new solver object after a reset. As only the API solver has write access to this, it is moved to the Solver::setInfo() method.
With this PR, all internal code is properly guarded against erroneous (and reckless) changing of options.
Fixes cvc5/cvc5-projects#12.
- Remove --build from GMP configure line (#8752)
This is an attempt to fix the pypi build.
- Relax an assertion in the evaluator (#8751)
In a rare case this can throw after https://github.com/cvc5/cvc5/pull/8740, complaining that `(/ 0.0 0)` and `(/ 0.0 0.0)` are not the same.
- Ensure substitutions in nonlinear solver are properly typed (#8748)
We would apply substitutions between int and real terms, effectively hiding the intness of variables from the coverings solver.
Fixes #8744.
The example from #8744 times out after the fix, thus no regression.
- Fix some issues with the Python API tests (#8746)
This PR addresses a few issues in the Python API:
the implementation of defineFunsRec() lacked the call to the C++ function
a bunch of tests for defineFunsRec() were missing
the test for getInstantiations() was incorrectly named and thus not valled.
add missing test for hashing of Sort
- Add test coverage for almost everything from the Java API (#8723)
This PR adds tests for almost everything that is not yet covered by the java API tests.
- Compress debug symbols to make libcvc5 smaller (#8743)
This adds `-gz` which compresses the debug symbols to make debug builds smaller. In my setup, `libcvc5.so` shrinks to about half its size from ~450MB to ~225MB.
- Improvements for evaluation in model (#8738)
This marks APPLY_SELECTOR and SEQ_NTH as unevaluatable kinds.
This means that get-value applied to applications of them e.g. (seq.nth t) will evaluate to c if (seq.nth t) is in the same equivalence class as constant c. (Note that this could be further improved to reason by congruence for (seq.nth s) where s = t, which I'm considering to do on a followup PR).
This removes many of the required -q from the command line arguments of our regressions. This also does some minor cleanup to our regressions to remove -q from further regressions.
- Do not depend on subtyping for APPLY_UF in TPTP parser (#8737)
- Add unit tests for getInstantiations (#8741)
- Do not rely on subtyping in real-to-int preprocessing pass (#8732)
- Disable proof testers for delicate regressions. (#8735)
This PR disables regress2/nl/ufnia-factor-open-proof.smt2 benchmark which fails with some debug builds in the nightlies. We should consider adding an option to disable testers under certain build configs. This PR also ensures that the lfsc tester displays all the options used to generate the LFSC proof.
- More preparation for strict type rules (#8733)
This is work towards making equalities and substitutions between terms of equal types.
- Fix proofs for ppAssert for theory Bool (#8708)
Fixes #8705.
This also impacts unsat cores when proofs are enabled.
- Fallback for sequential substitution proof reconstruction (#8730)
This makes our proof reconstruction fallback to a trivial sequential reconstruction in very rare cases where a sequential substitution fails to reconstruct. This can happen in some rare cases where terms are used in the domain of a substitution that otherwise would be modified by earlier substitutions. This occurs on 2 QF_SLIA benchmarks, attached is a delta-debugged version.
This also changes a warning message to a trace for this case, as a warning message may cause LFSC proof checking to fail when it should just give a warning for a TRUST_SUBS step, which is the default behavior regardless.
- Eliminate arithmetic subtyping for (dis)equalities from TPTP parser (#8724)
Towards making equality strictly typed / eliminating arithmetic subtyping.
- Separate ill-typed portion of arith models (#8734)
This makes it so that the ill-typed portion of arithmetic models is not included in the main arithModel map.
Conceptually, we should not include entries in the arithmetic model that violate type constraints since these should never be used e.g. in non-linear to justify whether a model is correct. Instead, by not including that value, we assume that no value was given for that variable. Sanity checking of the arithmetic model then needs only to access the ill-typed portion of the model directly.
This makes it so that strict type invariants can be enforced in the non-linear solver's model.
- Fix LFSC side condition for matching premise of concat_unify (#8726)
Occurs in QF_SLIA/20180523-Reynolds/pyex/peterc-pyex-doc-cav17-td/pymongo/pymongo-mongoclient/cc647bd246e485aa31a4dc8978e5211a7c1336911d1bfc78b45ee679.smt2 after 464 seconds on my machine.
- Add test coverage for almost everything from the Python API (#8720)
This PR adds tests for almost everything that is not yet covered by the python API tests.
- Preparation for making equality strictly typed (#8728)
This changes several places in arithmetic so that it never generates equalities between and an Int and a Real.
It also changes several uses of mkConstReal on integer values with mkConstInt whenever their type does not matter.
Since we do not construct CONST_INTEGER yet, this PR has no behavior change yet.
- Fix cache in learned rewrite preprocessing pass (#8725)
Fixes #8722.
- Fix more issues with subtypes in regressions (#8727)
In preparation for making type rule for equality strict.
- Add operators table.aggr and table.join (#8681)
- Use purification for set comprehension reduction (#8711)
Currently, the reduction lemma does not purify set comprehension from its reduction predicate. This means that our rewriter (if it were smart enough) should rewrite the reduction predicate to true.
Moreover, a new forthcoming model-based instantiation technique was giving wrong answers when set comprehensions were present since it could prove the reductions were tautological.
- Improve finding Python library/includes (#8718)
On macOS, find_package(PythonLibs ...) does not find the Python
include directory or library when they were installed via homebrew.
find_package(Python ...) is more robust, but only available on newer
versions of CMake. If we are compiling cvc5 on macOS and we have a newer
version of CMake available, this tries to use find_package(Python ...)
to find the paths.
- fix link to `Testing cvc5` in `INSTALL.md` (#8675)
The current link renders strangely and does not lead to the relevant subsection. This PR fixes that.
- Make equality solver the entry point for all equality engine explanations in arithmetic (#8719)
This makes it so that EqSolver is the main entry point for all equality engine explanations in arithmetic; it still defers to the CongruenceManager to compute these explanations.
To do this, when the core linear solver depends on an explanation from the equality engine, it instead provides a placeholder. Since explanations are computed recursively in TheoryEngine, this will trigger another call to TheoryArith::explain, which will then be handled by the EqSolver. Thus, there should be no net effect on the overall explanations in this commit.
This is work towards eliminating the dependency of the linear solver on the equality engine.
- Make printStatisticsSafe public (#8721)
Solver::printStatisticsSafe() is private right now. There is no real reason for that, and as we claim that the driver is only using the regular API we should just make it public.
- Add declareOracleFun interface to SolverEngine (#8622)
After this PR, declare-oracle-fun will be added to the API and parser.
- Refactor oracles using new std::function backend (#8717)
This also updates several places to be generalized to methods that return a vector of Nodes. Previously we had assumed a use case returning a single node.
After this PR, #8622 will be updated to use the new std::function interface.
- Remove unecessary calls to equality engine from congruence manager (#8715)
Removes a deprecated explain interface.
- Remove obsolete private methods from API (#8716)
This PR removes two private utilities from the API: Sort::sortSetToTypeNodes and one DatatypeDecl constructor.
- Fix rewrite for to_real in division by zero (#8714)
Fixes #8712.
- Add support for oracle constant nodes (#8707)
This is the beginning of a refactoring to make std::function the basis for oracles internally, not binary names.
- Fix LFSC node converter for 0-ary tuples (#8706)
Was missing 0-ary Tuple case for type-as-node.
Also removes a spurious check in the user-defined sorts case.
Fixes some issues in the nightlies.
- Update LFSC version (#8713)
This updates the get-lfsc-checker script to get the latest version of
LFSC, which supports older versions of CMake.
- Use (non-recursive) unpurified form instead of original form for defining Skolems (#8699)
This modifies our treatment of purification Skolems in the internal proof calculus. In particular, we now use an "unpurified form" instead of "original form" for defining Skolems. SKOLEM_INTRO is modified to prove the equality between a skolem and its unpurified form.
For example:
k1 purifies (ite A B C)
k2 purifies (+ k1 1)
The unpurified form of k2 is (+ k1 1), its original form is (+ (ite A B C) 1).
As a consequence:
(1) Our global skolem sharing is now slightly weaker, for example a k3 could be constructed whose unpurified form is (+ (ite A B C) 1); previously this would guaranteed to be k1.
(2) We do not require recursively computing the original form of terms when constructing purification Skolems,
(3) The witness form proof generator requires a fix point.
(4) The LFSC signature is simplified, and does not require a side condition to recursively compute the original form of a Skolem.
Fixes cvc5/LFSC#81.
- docs: Some fixes in options docs. (#8710)
- Change option name for mbqi in fmf (#8701)
In preparation for a new basic implementation of MBQI.
- Simplify representation of datatypes at the TypeNode level (#8702)
They previously were TYPE_CONSTANTs hashed by the index of their DType in the NodeManager. Now they are variables having an attribute that is their index.
This makes datatypes more analogous to uninterpreted sorts, and eliminates the need for an auxiliary DatatypeIndexConstant class.
- Final preparation for CONST_INTEGER (#8700)
With this PR, CI passes when using CONST_INTEGER instead of (all) integral CONST_RATIONAL.
This does not make this change yet, so CONST_RATIONAL is still used throughout.
- Migrate basic EqualityEngine management from CongruenceManager to EqSolver (#8684)
This is work towards having the linear arithmetic solver not impose restrictions on equalities.
The linear arithmetic solver using a CongruenceManager which involves many non-standard uses of the equality engine.
The responsibilities of the CongruenceManager should be migrated to the arithmetic EqSolver, which manages the equality engine in the default way.
This PR is the first step. It makes it so that the memory management and notifications of the equality engine are now solely the responsibility of the EqSolver.
All relevant notifications from the EqSolver are directly forwarded to CongruenceManager. Thus there are no significant behavior changes in this PR.
This PR required removing the experimental option arithCongMan, which forces having the CongruenceManager and the EqSolver both use equality engines.
- Add strict-cube and decision-trail partitioning strategies (#8651)
Add the strict-cube modification to the revised partitioning algorithm and add the full-trail partitioning strategy.
- More robust treatment of flattening in arith rewriter (#8695)
Currently can allow rewritten forms to be rewritable.
Fixes #8692. Fixes #8693. Fixes #8697.
- Make arith msum utility agnostic to Int (#8694)
This utility should continue to assume arithmetic subtypes.
Fixes #8691.
- Add missing tests for some corners of the API (#8688)
This PR adds a bunch of unit tests for some not yet covered corners of the API.
- docs: Do not use explicit line numbers in literalinclude. (#8690)
- Further refactoring in preparation for CONST_INTEGER (#8687)
Miscellaneous refactorings from trying to enable CONST_INTEGER.
- Fix tuple printing in LFSC (#8696)
We weren't collecting them as user-defined types after the recent refactor to Tuples.
- 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.
- 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.
- Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686)
This PR removes the usages of CONST_RATIONAL in the nonlinear arithmetic solver.
- 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
- 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".
- 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.
- 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.
- Make extended rewriter use standard Subs utility (#8682)
This is work towards ensuring all substitutions are strictly typed.
- Add an option to enable all testers. (#8676)
- Add missing parenthesis for bags documentation (#8673)
- 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.
- 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.
- 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.
- 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/.
- 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.
- Move datatype split inference scheme to its own method (#8664)
- Clean code for datatypes split (#8667)
Non-moving version of #8664.
- 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.
- Fix PyUnicode_AsWideCharString signature (#8522)
Add proper exception specification to the `PyUnicode_AsWideCharString` signature.
- 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.
- Add option to apply constant propagation for all learned literals (#8668)
Adds `--simplification-bcp`, disabled by default.
- 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.
- Minor improvements for entailment test (#8663)
Makes some minor improvements to the existing (non-incremental) entailment tests, based on comparing with a new implementation.
- Minor improvements to quantifiers utilities (#8661)
- 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
- Move rep set iterator to its own file (#8647)
- 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.
- 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.
- 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.
- Simplify internal represenation of uninterpreted sorts (#8660)
- 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).
- 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.
- [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.
- 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.
- Option exception for quantified bit-vectors + eager bitblasting + incremental (#8658)
Fixes #8654.
- Make BVInstantiatorUtil an EnvObj (#8633)
Eliminates 5 of the remaining 8 static calls to Rewriter::rewrite.
- 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>
- Minor cleanup of NodeManager (#8650)
- 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.
- 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.
- [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.
- Add bag.partition evaluation (#8637)
- Add utilities in preparation for deep restarts (#8642)
- 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`.
- 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).
- Add declare-oracle-fun command (#8621)
In preparation for adding declare-oracle-fun to the API/parser.
- 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)).
- 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.
- 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.
- 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.
- Avoid trivial equalities in explanation of SETS_CARD_CYCLE (#8635)
This was the root cause of cvc5/cvc5-projects#178.
- Simplify implementation of subtype methods in TypeNode (#8634)
Also deletes unused data that was used for an inference schema involving subtypes in sets.
- 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
- 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.
- 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.
- 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
- Add some missing FP symbols to LFSC (#8629)
- 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.
- Make more utilities distinguish Int and Real (#8626)
Towards eliminating arithmetic subtyping.
- 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.
- 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
- 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.
- 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.
- 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.
- Implement internal support for synthesis modulo oracles (#8617)
SyMO is implemented as a preprocessor for SMT queries in the verification subsolver of SyGuS.
- 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.
- 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.
- 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.
- [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
- 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.
- Fix spurious assertion involving subtypes (#8611)
Fixes #8609.
- Update LFSC version (#8614)
Now has a different expected output ("success" for each check).
- Add Relation and Table types to SMTLib parser (#8605)
- Fix type issue for FP constants in LFSC node converter (#8612)
Fixes type errors in debug builds.
- V411-001 allow setting of ar in cadical Makefile
Change-Id: Ibcd22da42a7777adbbf2990cfd4e4f05ed551efc
- 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.
- 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.
- 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).
- 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.
- 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.
- Fix more misuses of arithmetic subtypes (#8601)
- [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
- More cleaning uses of arithmetic subtyping (#8595)
Towards eliminating arithmetic subtyping.
- 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.
- Remove spurious case of ppRewrite (#8596)
Constants equal to constants are always rewritten to false.
- 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.
- V411-001 improve compilation on windows
using NO_CMAKE_FIND_ROOT_PATH seems to be required for cross
compilation, otherwise the configure script doesn't find the
libraries. It seems to be OK for linux build as well
Change-Id: Iec7cb4e7f1549f73f714eefeb7302c532435f1e3
- V411-001 merge cvc5 1.0.0 into Adacore sources
Change-Id: Ibb8929e081164d126ff7a3d826ad2d59afc38e73
- 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.
- Minor refactoring of smt2 printer (#8588)
- 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.
- 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).
- 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.
- 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.
- 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.
- Add method to get leaves of a NodeTrie (#8583)
From the oracles branch.
- 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
- Eliminate SmtSolver dependency on SolverEngineState (#8581)
This is in preparation for making SmtSolver able to be deep reset (reconstructed) within in a SolverEngine instance.
- Minor fix for printing nullary operators in smt2 (#8577)
- Fix proof checker for SUBS (#8578)
Could lead to proof checking failures when using `--proof-granularity=rewrite`
- Fixes for LFSC printing and signatures (#8579)
Ensures we recognize some internal FP symbols, adds a missing string operator, fixes seq.unit operator printing (required for CONG over seq.unit), fix for 0-ary tuple printing.
- Start post-release for 1.0.0
- Bump version to 1.0.0
- api: Fix doc generation for kinds in java API. (#8576)
Plus some more fixes for docs.
- Update copyright headers for release 1.0 (#8539)
- Update NEWS for cvc5 1.0. (#8460)
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
- Make inst constant attribute robust to purification variables (#8573)
Fixes #8572.
Certain combinations of cegqi/sygus-inst may be solution unsound when combined with E-matching, due to using skolems that have dependencies on instantiation constants are used in instantiations.
- Make rewriter more robust against RAN becoming rational (#8564)
We use real algebraic number to represent multiplicities of sum terms within the arithmetic rewriter. Unfortunately, such real algebraic numbers can realize that they are in fact rational at awkward times. This makes isRational() unsuitable for checking this, instead we should construct the node and check afterwards.
- api: More fixes in the java API. (#8571)
- Be permissive for subtyping in function definitions (#8568)
This is to accommodate the Real theory in SMT-LIB, which says that numerals specify reals.
Instead of making our parser for numerals dependent on the logic, we are more permissive.
This fixes several spurious parsing issues in smtlib.
- api: More fixes in C++ API docs. (#8570)
- Write-up for Pythonic API quickstart (#8566)
- docs: Fix mkTerm calls in theory documentation. (#8567)
- api: Fix OptionInfo docs for java API. (#8569)
- api: Fixes in docs for Op. (#8565)
- api: Fixes for Grammar docs in java API. (#8563)
- api: Fixes in java api docs. (#8562)
- api: Fixes in docs for DatatypeConstructor. (#8561)
- Docs: remove api from package name in java.rst (#8560)
Fix broken links in https://cvc5.github.io/docs/cvc5-0.0.12/api/java/java.html
- api: More fixes in docs. (#8559)
- api: First batch of fixes in the api docs. (#8558)
Uses `@return <uppercase> .... <period>` and `@param <param> <uppercase> ... <period>`,
plus various fixes in the docs.
- Fix links when converting kinds documentation to python (#8557)
This mainly fixes explicit rst links when we convert the kinds comments to python.
- python api: More fixes. (#8556)
- Start post-release for 0.0.12
- Bump version to 0.0.12
- Maintain symlink to docs for latest release (#8555)
This PR creates/updates a symlink called latest to the last release. This simplifies permalinks into the documentation.
- Remove duplicate lines (#8552)
We remove the arguments from links to solver methods in the Kinds
documentation to turn C++ references into python references. This
oftentimes collapses previously different overload of methods (usually
mkTerm()). This PR generically removes duplicate lines from these
comments using some re magic.
- Bump Pythonic (transcendentals) & exception example (#8553)
- Bump version of Pythonic API to include transcendentals.
- Document Pythonic API's transcendentals.
- Add exception Pythonic API example.
- api: Various fixes in Python documentation. (#8554)
- Various improvements and fixes in the documentation (#8551)
This PR contains a variety of fixed and improvements to the documentation.
- Rename getInstantiatedConstructorTerm to getInstantiatedTerm (#8549)
This is in line with the change for non-parametric constructors (getConstructorTerm -> getTerm).
Also adds documentation to make the use of constructors, selectors, testers, updaters more clear.
- Use raw symbols in proofs (#8550)
This ensures we don't quote symbols that should not be quoted, fixing two issues:
(1) Proofs in the internal calculus don't convert `:args` to `|:args|`.
(2) LFSC identifiers for terms are not quoted based on SMT-LIB restrictions.
Work towards https://github.com/cvc5/cvc5-projects/issues/466, quoted TypeNode names still need to be addressed.
- [proofs] [sat] Make SAT assumption bookeeping robust to incremental (#8536)
Similarly to what happened with proofs of optimized SAT clauses getting lost (in the sense of inserted at lower assertion levels than the current one, during incremental solving), we need to make the bookeeping of the current SAT assumptions in the SAT proof manager robust to context popping. Not doing so can break the final proof construction, which relies on this information. A regression is added which showed the issue via the openness of a step added to the lazy proof chain (even though this did not lead to issues in the final proof).
This commit extends the OptimizedClausesManager to also optionally track a hash set of nodes to have nodes added to it during popping. This is hooked in the SAT proof manager to the SAT assumptions hash set.
There are four instances of notifications to the SAT proof manager of SAT assumptions: two in the proof CNF stream and two in the SAT solver. We only need to worry about the proof CNF stream ones, since the SAT solver ones are for literals (which do
not have assertion levels) and for some cases of the final conflict clause generated, which is always at the current assertion level. For the proof CNF stream ones it suffices to notify the SAT proof manager when the CNF stream itself is notified that a propagation or clause was inserted at an optimized level, as these are the only possible cases.
- Fix for get-value with empty uninterpreted sort domain (#8547)
Alternative for https://github.com/cvc5/cvc5/pull/8546.
We were mistakenly using `mkGroundTerm` instead of `mkGroundValue` to make the domain of an uninterpreted sort non-empty.
This ensures that get-value calls do not throw a spurious exception when there is a declared uninterpreted sort and there are no terms of that sort.
As a result, this also required fixing a few further issues regarding how uninterpreted sort constants are printed in models, and fixing the expected results on 2 more regressions.
- Start post-release for 0.0.11
- Bump version to 0.0.11
- use one process more than we have cores (#8545)
This PR uses one process more than we have cores in the CI. This speeds up the CI jobs when time is spent waiting on IO instead of actually using the CPU.
- Rename mkSygusGrammar to mkGrammar (#8544)
- Remove variant of mkDatatypeDecl with one sort parameter (#8543)
Subsumed by the vector version.
Also marks more methods as experimetnal.
- api: Rename get(Selector|Constructor)Term() to getTerm(). (#8537)
- Follow renaming within pythonic API (#8532)
We are renaming files in the pythonic API to make it look less like it is somehow part of z3 (but still acknowledge that we took code from z3Py properly). This PR follows the change in cvc5/cvc5_pythonic_api#80.
- Always cancel already running CI runs on forks (#8542)
One effect of our changed concurrency policy is that we never cancel runs on forks. This PR changes this, always allowing the concurrency mechanism to cancel on repositories that are not the main repository.
- Minor edits in docs. (#8540)
- Ignore irrelevant exponential terms (#8534)
Fixes #8517.
- docs: Add Python installation instructions for pip. (#8538)
- api: Remove DatatypeConstructor::getSelectorTerm(). (#8535)
- Require that used model values are constant in CEGQI (#8528)
Fixes #8520.
- Add a few miscellaneous pieces of documentation (#8533)
- Remove java API methods that accepts lists as arguments (#8541)
This PR removes some unnecessary methods in the Java API that were added to simplify several unit tests that use dynamic arrays. The goal is to make the java API consistent and as small as possible.
Users could use asList, toArray methods to use generic lists if they wish.
- Add more explanations in the API (#8493)
This also removes a few references to "first-order constants" (using "free constant" instead) since mkConst can be used to construct higher-order free constants.
- Simplify the python base API in a few places (#8514)
This PR simplifies a few methods in the python base API.
- Simplifications to the datatypes API (#8511)
This PR makes it so that common users of the datatypes API do not need to use "unresolved" datatypes sorts. Instead, these are automatically inferred by the NodeManager when calling mkMutualDatatypeTypes.
API Changes:
(1) adds addSelectorUnresolved to DatatypeConstructorDecl, which is the sole method needed to specify ordinary recursive selectors.
(2) adds to unit test examples that use this variant instead of using unresolved sorts.
(3) the API method mkUnresolvedSort is renamed to mkUnresolvedDatatypeSort and is marked experimental.
Note that unresolved datatype sorts are still needed to support mixed parametric datatypes and nested recursive datatypes in the smt2 parser, so they cannot be deleted yet.
Followup PR will add to documentation on elaborate further on how to use the datatypes API.
- docs: Document UnknownExplanation. (#8508)
- Prevent using the coverings solver with extended operators (#8523)
The way we construct the model within the nonlinear extension makes using multiple subsolvers that contribute to the model potentially unsound. This PR prevent the coverings solver from being used if extended operators are present, unless --nl-cov-force is given.
Fixes #8515. Fixes #8516.
- api kinds: Refactor docs for kinds to properly render in Python. (#8510)
- api: Remove Datatype::getConstructorTerm(). (#8529)
- Replace regression by minimized one via ddSMT (#8531)
- Only run pypi packaging when release is published (#8526)
We incorrectly triggered pypi packaging when a release was created or published, i.e. it would run twice.
- make-release: Clarify instructions for pushing commits and tag. (#8524)
- [proofs] [doc] Document string rules (#8498)
Also replaces negation of equality literals by disequality literals.
- Change CI concurrency policy to not queue on main (#8530)
Previously, we would only allow one job per branch/PR and only cancel old jobs on PRs.
This PR changes this policy to allow multiple jobs at once on main.
The way this is done basically follows https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#example-using-a-fallback-value.
- Document special member functions in python API (#8513)
This PR documents relevant special member functions __getitem__ and __iter__ for some classes in the base python API.
- Python API: Do not rename enumerators. (#8507)
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
Co-authored-by: Gereon Kremer <gkremer@stanford.edu>
- [proofs] [alethe] Fix Alethe post-processor (#8525)
Previously the Alethe post-processor was merging subproofs, which should not be done at this stage. As a consequence some post-processed proofs were becoming open.
- Start post-release for 0.0.10
- Bump version to 0.0.10
- Internal simplifications to constructing datatypes (#8519)
In preparation for #8511.
This makes it so that unresolved sorts are automatically inferred when constructing datatypes at the NodeManager level. This is in preparation for simplifying the API.
Changes:
(1) NodeManager is cleaned so that unresolved types are automatically inferred and are not a part of its public interface. Internal code generating datatypes is simplified as a result.
(2) Adds ne…
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A lot of the naming still suggests that this is somehow part of z3. While we incorporate code from z3 (and still acknowledge this), we now call everything
cvc5_pythonic_api.