summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-04Revert semantic change from refactoringfixInConflictAndres Noetzli
In PR #3398, a minor change was introduced: One of the checks for whether there is a conflict or not was flipped (https://github.com/CVC4/CVC4/pull/3398/files#diff-62fffb0d9df0385909621e424bdcef72R1652). This commit reverts that change.
2020-02-03Regression tests for arithmetic proofs. (#3701)Alex Ozdemir
* Add more arith proof regression tests These tests are designed to test interesting cases of arithmetic proofs, such as mixing integers and reals and tightening bounds. Right now, they have the --no-check-proofs flag set, which prevents them from testing the proof machinery. However, once we check that machinery into master, we'll remove that flag, thus enabling the full effect of the tests. * A few comments explaining things. * Add another tightening test * Add new test to CMake * No --no-check-models. There are no models anyway. * Delete smt-lib-version, per Yoni
2020-02-03Increase regression test time limit to 1200s. (#3704)Aina Niemetz
Fixes #3565.
2020-02-03Fix corner case - might need to REWRITE_AGAIN (#3706)Clark Barrett
2020-02-03Utility function for getting component types (#3703)Andrew Reynolds
2020-02-03Minor fixes to regressions (#3702)Andrew Reynolds
Fixes two issues in regressions, fixes regress1.
2020-02-03Fix cardinality of uninterpreted types when univset is not used (#3663)mudathirmahgoub
* Fixed bug 3662 * format * small change * added bug3663.smt2 file * throw Logic Exception * throw Logic Exception * ;EXIT: 1 Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-02-03Fix corner case of empty domains in bounded fmf (#3690)Andrew Reynolds
2020-02-03Example inference utility (#3670)Andrew Reynolds
2020-02-02Renaming '--bsd' to '--no-gpl' (#3609)Andrew V. Jones
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
2020-01-31Handle `expectedType` in TheoryProofEngine (#3691)Alex Ozdemir
`TheoryProofEngine` now uses the `expectedType` optional argument. * When printing terms, it sets this for theories that it dispatches too * It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation. * It is mindful of `expectedType` when using the let map. I also moved to hpp function implementations into the cpp.
2020-01-31Allow PBE symmetry breaking with sygus stream (#3686)Andrew Reynolds
2020-01-31Refactor relevance vectors for asserted quantifiers (#3666)Andrew Reynolds
2020-01-31Update sygus grammar normalization to use node-level datatype. (#3567)Andrew Reynolds
2020-01-31Refactor sygus stats (#3684)Andrew Reynolds
2020-01-31Minor refactoring of constructor classes in fast enumerator (#3685)Andrew Reynolds
2020-01-31Fix arithmetic rewriter for exponential (#3688)Andres Noetzli
2020-01-30Fix rep set increment for empty domains (#3682)Andrew Reynolds
2020-01-30Make eq chain an aggressive rewrite in extended rewriter (#3679)Andrew Reynolds
2020-01-30Eliminate spurious postprocessing step for single invocation (#3674)Andrew Reynolds
2020-01-30Ensure literals in FMF decision strategies are in the CNF stream (#3669)Andrew Reynolds
2020-01-30Weaken assertion for models with approximations (#3667)Andrew Reynolds
2020-01-30Move disequality list to solver state in strings (#3678)Andrew Reynolds
2020-01-30Example minimize evaluation utility. (#3671)Andrew Reynolds
2020-01-30External cache argument for evaluator (#3672)Andrew Reynolds
2020-01-30Do not debug check model for models with approximations (#3673)Andrew Reynolds
We don't run check-model for models with approximate values, however we were still running the internal debugCheckModel method, which leads to assertion failures. This disables this check. Fixes #3652.
2020-01-29Better heuristics for marking congruent variables (#3677)Andres Noetzli
2020-01-29Modularize more steps in the strings strategy (#3676)Andrew Reynolds
2020-01-29Minor updates to string utilities (#3675)Andrew Reynolds
2020-01-29expectedType in proof-printing code (#3665)Alex Ozdemir
* expectedType in proof-printing code To print lemma proofs in theories that use multiple sorts that have a subtype relationship, we need to increase communication between the TheoryProofEngine and the theory proofs themselves. This commit add an (optional) argument `expectedType` to many term-printing functions in TheoryProofEngine and TheoryProof. Right now it is unused, so always takes on the default value of "null" (meaning no type expectation), but in the future the TheoryProofEngine will use it to signal TheoryProof about what type is expected to be printed. * TypeNode, Don't mix default args & virtual * Use TypeNode instead of Type (The former are lighter) * Don't add default arguments to virtual functions, because these cannot be dynamically overriden during a dynamic dispatch. * Since we don't want them to be overidable anyway, we use two functions: one that is non-virtual and has a default, the other that is virtual but has no default. The former just calls the latter. * clang-format after signature changes
2020-01-29Fix isLeq function in String utility (#3659)Andrew Reynolds
2020-01-28Do not insist on bound values being constant in arithmetic instantiation (#3643)Andrew Reynolds
2020-01-28Avoid PLUS with one child for bv2nat elimination (#3639)Andrew Reynolds
2020-01-25Axioms for affine function bounds. Tests. (#3632)Alex Ozdemir
* Axioms for affine function bounds. Tests. * Apply suggestions from code review Co-Authored-By: yoni206 <yoni206@users.noreply.github.com> * Clarify descriptions of th_lira tests Thanks, Yoni! Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
2020-01-23Fix trivial solve method for single invocation (#3650)Andrew Reynolds
2020-01-22Fix subtyping for instantiations where internal representatives are chosen ↵Andrew Reynolds
(#3641)
2020-01-22Fix substitution in nl solver (#3638)Andrew Reynolds
* Fix for 3614 * Add regression * Remove regression Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-01-22Fix single invocation partition for non-function non-atomic types (#3642)Andrew Reynolds
2020-01-22Fix check for subtypes in sygus PBE (#3640)Andrew Reynolds
2020-01-22Fix parameteric sorts involving Booleans in sygus default grammars (#3629)Andrew Reynolds
2020-01-21Types and side conditions for affine bounds (#3631)Alex Ozdemir
* Types and side conditions for affine bounds Bounds (being positive, non-negative) actually have an arithmetic. This PR defines that. Useful b/c Farkas proofs are basically just sums of bounded affine functions. * Address Yoni's comments. Thanks! * Moved a positivity-test to th_real * Describe what an affine bound is in better detail
2020-01-21Affine Axioms (#3630)Alex Ozdemir
Used for proving that real terms are affine functions of their variables.
2020-01-21Types & side-conditions for linear and affine fns (#3627)Alex Ozdemir
This commit introduces types for linear combinations of arith variables along with side conditions for their arithmetic. It does the same for affine functions. These primitives are ultimately used in our machinery for Farkas proofs.
2020-01-21Axioms (and side conditions) for tightening bounds (#3613)Alex Ozdemir
* Axioms (and side conditions) for tightening bounds * Side conditions for verifying floor/ceiling-like functions * Axioms for their correct execution * Axioms for bound tightening. * Apply suggestions from code review Co-Authored-By: yoni206 <yoni206@users.noreply.github.com> * Address Yoni's comments by addings documentation. Thanks Yoni! Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
2020-01-17LIRA proof: Arithmetic predicates & reification thereof (#3612)Alex Ozdemir
* Merge branch 'master' into lira-pf-arith-pred * Shorten reify_arith_pred, thanks Yoni! Use recursion! * typo
2020-01-17LIRA sig: int, real terms, and conversions (#3610)Alex Ozdemir
* LIRA sig: int, real terms, and conversions * Address Yoni's comments. * Better description of "reify" functions * explicit (rather than implicit) `fail` when reifying integer division Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
2020-01-17Use axioms when checking goal entailment for abduction algorithm (#3611)Andrew Reynolds
2020-01-15New C++ API: Add nullary constructor for Result. (#3603)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback