summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2020-03-31Convert more uses of string-specific functions (#4158)Andrew Reynolds
Towards theory of sequences.
2020-03-30Rewrites for all remaining return statements in strings rewriter (#4178)Andrew Reynolds
Towards proofs for string rewrites. All return statements all now associated with an enum value. An indentation in a block of code changed in rewriteMembership.
2020-03-30Support indexed operators re.loop and re.^ (#4167)Andrew Reynolds
Towards support for the strings standard. This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices). This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions. Also fixes #4161.
2020-03-30Remove ref skolem datatype option (#4185)Andrew Reynolds
Fixes #4180, fixes CVC4/cvc4-projects#133, fixes CVC4/cvc4-projects#134.
2020-03-30Frontend support for the choice operator (#4175)mudathirmahgoub
Added the operator choice to Smt2.g and Cvc.g. Removed the unused parameter hasBoundVars from TheoryModel::getModelValue
2020-03-28Enumeration for String rewrites (#4173)Andrew Reynolds
In preparation for string proof infrastructure. This introduces an enumeration type to track string rewrites. It also makes inference printing more consistent.
2020-03-27Split transcendental solver to its own file (#4156)Andrew Reynolds
* Attempting to split transcendental function solver * Clean * Format * More * Format * Attempt link * Format * Fix * Another refactor * More * More * Rename * Format Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
2020-03-27Move string utility file (#4164)Andrew Reynolds
Moves the string file to string.h. This is required since other required utilities will soon need to be added to regexp.h.
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
Work towards support for the strings standard. This updates the string solver and parser such that: The internal representation of strings is vectors of code points, Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models, The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings, Handle unicode escape sequences according to the SMT-LIB standard in String, Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary, Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points.
2020-03-26Added unit-cube-like test for branch and bound (#3922)Amalee
* unit-cude test wip * test for wip unit cube test * fixed simple rounding * wip * Passing tests except for sat vs unknown ones * added flag for cube test * put example back to normal * Fixed for style guidelines. * fixed rewrite bug * removed extra comments * unit-cude test wip * test for wip unit cube test * fixed simple rounding * wip * Passing tests except for sat vs unknown ones * added flag for cube test * put example back to normal * Fixed for style guidelines. * fixed rewrite bug * removed extra comments * Small fixes based on PR feedback * replace NodeManager::currentNM with nm and clang formatted * renamed test * Added a regression test that triggers branch and bound * Added ; COMMAND-LINE: --arith-brab * Updated arith-brab test * arith-brab enabled by default * Added --nl-ext-tplanes to regress0/nl/ext-rew-aggr-test.smt2 Co-authored-by: Amalee Wilson <amalee@cis.uab.edu> Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
2020-03-26Add stats for string reductions, lemmas and conflicts (#4149)Andrew Reynolds
This PR adds comprehensive stats for reductions, lemmas and conflicts in TheoryStrings. Remaining stats will track all inferences (which are finer grained steps that may lead to lemmas/conflicts). Additionally this PR refactors calls to OutputChannel::lemma in TheoryStrings / InferenceManager. There are now only 2 calls to lemma(...) during registerTerm(...), one for "atomic" string terms (corresponding to length splits typically) and one for non-atomic terms.
2020-03-26Generalize more string-specific functions (#4152)Andrew Reynolds
Towards theory of sequences. Note this PR also changes design in core/base solver. Previously I had estimated that we should have separate instances per type for these solvers, but I think it is better to have these classes handle all string-like types simultaneously. This means they should not have a d_type field.
2020-03-25Care graphs based on polymorphic operators in strings (#4150)Andrew Reynolds
Towards theory of sequences. To compute a care graphs, we need to group function applications by the string type they are associated with. This PR introduces a utility to function to get the "owning string type" for a function application, and updates the care graph computation so that it partitions function applications according to this type.
2020-03-25Support async-signal-safe printing of inferences (#4148)Andres Noetzli
Commit c9b7c3d introduced code for counting the number of string inferences done per type of inference. However, it did not add support for printing the inference names in an async-signal-safe manner via safe_print() (note that printing in signal handlers is done differently from the regular stats printing). This commit adds the corresponding code, s.t. we get the inference names when printing the stats when CVC4 is interrupted or crashes.
2020-03-25 Generalize more uses of string-specific functions (#4145)Andrew Reynolds
Towards theory of sequences.
2020-03-24Restrict partial triggers to standard quantified formulas (#4144)Andrew Reynolds
Fixes #4143.
2020-03-23Restrict cases of sygus grammar reduction based on argument variants (#4131)Andrew Reynolds
An assertion is triggered for some V2 versions of SyGuS V1 benchmarks during sygus grammar reduction. This PR updates this technique so that it only applies to sygus constructors whose sygus operators are lambdas of the form lambda x1 ... xn. f( x1 ... xn ). FYI @abdoo8080 .
2020-03-23Infer when sygus operators are equivalent to builtin kinds (#4140)Andrew Reynolds
The V2 parser always turns sygus operators into lambdas for consistency. This PR ensures that we nevertheless infer when a sygus operator is equivalent to a builtin operator, e.g. (lambda x y. (+ x y)) is equivalent to +. The main reason this is required is to ensure that solution reconstruction heuristics work optimally when we make the switch SyGuS V1 -> V2 (see 5 failing benchmarks due to --cegqi-si=all on #4136).
2020-03-23Simplify auxiliary variable handling in CEGQI (#4141)Andrew Reynolds
Fixes #3849 and fixes #4062. Overall, the effect of this PR is that CEGQI will generate better instantiations more frequently for quantified formulas that involve the introduction of auxiliary variables. In CEGQI, auxiliary variables introduced in CEX lemmas must be given special treatment (since the instantiations should not involve them, thus they must be solved for as well). Previously, auxiliary variables that are introduced as parts of CEX lemmas were currently assumed to be: (1) Only occurring from ITE removal, e.g. s[(ite C t1 t2]) ---> s[k] ^ ite( C, k = t1, k = t2 ) (2) Always trivially solvable by looking at which literal was asserted (k = t1 or k = t2). Both of these assumption do not hold in general (aux variables can come from other kinds of terms e.g. choice functions, and the user can force options that rewrite arithmetic equalities to inequalities). This makes auxiliary variable handling in CEGQI more robust by treating auxiliary variables as standard variables. Effectively, this means that the entire procedure for determining instantiations is run for auxiliary variables. This PR removes the specific hacks that were used previously that were based on the assumptions above. Additionally, #3849 triggered a second issue: SyGuS solution reconstruction that involves auxiliary variables that are introduced as part of instantiation lemmas should not be considered valid solutions. Previously, only a warning was given.
2020-03-23Throw exception for non-well-founded unimplemented SyGuS types. (#4125)Andrew Reynolds
Fixes #3931. Currently we print a warning for unimplemented types when constructing default SyGuS grammars. We should additionally throw an exception when the unimplemented type would lead to a non-well-founded datatype.
2020-03-23Change transcendental function app slave list to unordered_set (#4139)Andrew Reynolds
Fixes #4112.
2020-03-22Collect statistics about normal form inferences (#4127)Andres Noetzli
This commit adds code to count the number of inferences made of each inference type for normal form inferences. It extends the Inference enum in `infer_info.h` and adds two new `sendInference()` methods in the `InferenceManager` to send and count inferences that have a corresonding entry in the `Inference` enum.
2020-03-22Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)Andrew Reynolds
Fixes #4092 and fixes #4134. Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.
2020-03-21Simplify heuristic in `processNEqc` (#4129)Andres Noetzli
This commit removes a special case in `CoreSolver::processNEqc()` where we stopped looking for inferences for a given normal form as soon as we found the highest priority inference (currently that an element in the normal form is empty). This effectively elevates the priority of this inference to the other inferences that are done immediately instead of being added to the `pinfer` vector that holds the possible inferences. The experiments that I've run seem to confirm that it is unnecessary to have this special case.
2020-03-20Generalize mkConcat for types (#4123)Andrew Reynolds
Towards theory of sequences. The utility function mkConcat needs a type to know what to construct in the empty string case.
2020-03-20Fix sort comparison within assertion in cegis (#4113)Andrew Reynolds
2020-03-20Guard cases of sort inference in quantifier free logics in uf cardinality ↵Andrew Reynolds
(#4074) Fixes #4068 and fixes #4085 and fixes #4063.
2020-03-20Split string-specific operators from TheoryStringsRewriter (#3920)Andrew Reynolds
Organization towards theory of sequences. The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.
2020-03-20Do not assign higher-order representative if function does not exist (#4073)Andrew Reynolds
2020-03-20Handle failures for sygus QE preprocess (#4072)Andrew Reynolds
If the user explicitly disabled the QE algorithm and asked for QE, then we should resort to normal methods. Fixes #4064 and fixes #4109.
2020-03-20Make handling of illegal internal representatives in quantifiers engine more ↵Andrew Reynolds
robust (#4034) Fixes #4002 (that benchmark is now unknown). The experimental option --cbqi-all previously had some issues when combined with finite model finding. When these two options are used simultaneously, it may be the case that certain equivalence classes are "illegal" since they contain only terms that are ineligible for instantiation. The previous code threw a warning when this occurred which in extreme cases allowed for potentially ineligible terms for instantiation. The new code is more conservative: we never choose illegal internal representatives and instead set the incomplete flag in finite model finding when this occurs. A block of code changed indentation in this PR, which was updated to the new standards.
2020-03-20Refactor enumerator for strings (#4014)Andrew Reynolds
Towards theory of sequences. This separates out a virtual base class and utility class for the strings enumerator, which will be extended for sequences later.
2020-03-19Only apply testConstStringInRegExp to const regexp (#4120)Andres Noetzli
Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites `(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements preceding `(_)*` match the empty string using `TheoryStringsRewriter::testConstStringInRegExp()`. However, this method only expects to be called on constant regular expressions (i.e. regular expressions without string variables). This commit adds a corresponding check before calling `TheoryStringsRewriter::testConstStringInRegExp()`.
2020-03-19Remove spurious assertion (#4117)Andrew Reynolds
Fixes #4106. The assertion was the wrong polarity (should have been Assert(options::cbqiAll()); but regardless is no longer an invariant of CEGQI).
2020-03-18Always enable cbqi literal dependency (#4116)Andrew Reynolds
Fixes #4105. It appears that the two (experimental) options in that issue were incompatible. A block of code changed indentation in this PR and was updated to guidelines.
2020-03-18Fix issue with multiple infinities in CEGQI for LIRA (#4114)Andrew Reynolds
Fixes #4086. Quantifier instantiation involves two symbolic representations of infinities for real and int and was not handled correctly previously.
2020-03-18Move node visitor class from smt_util/ to expr/ (#4110)Alex Ozdemir
Done by: Running rg 'smt_util/node_visitor' -l | xargs sed -i 's/smt_util\/node_visitor/expr\/node_visitor/' in src to change the #includes Moving the file Changing src/expr/CMakeLists.txt and src/CMakeLists.txt clang-format, omitting node_visitor.h. In reference to discussion, here.
2020-03-16clang-formatAlex Ozdemir
2020-03-16Fix simplicity check in propAlex Ozdemir
2020-03-16Fix antecedent loop. WhoopsAlex Ozdemir
2020-03-16Only save farkas+tightening proofs. Error on holesAlex Ozdemir
I'll remove the error later
2020-03-16Expand the definition of a "simple" farkas proof.Alex Ozdemir
Before, a "simple farkas proof" was one that just applied the farkas lemma. Now it allows for the antecedents to (optionally) be tightened. Note that hasSimpleFarkasProof was (and is) dead code. We will use it to decide whether to print a proof or a hole.
2020-03-16Create master equality engine at context level 0 (#4081)Andres Noetzli
Fixes #4077. The master equality engine in `TheoryEngine` was being created at SAT context level 1. If the context was popped to level zero by `(reset-assertions)`, `true` and `false` were removed from the master equality engine, which lead for example to `(= ((_ extract 3 3) x) (_ bv1 1))` and `(_ bv1 4)` being merged (this can be gathered from looking at `-t equality`). This commit fixes the issue by postponing the global context pushes until after the theory engine has been initialized.
2020-03-15Handle cases in --sygus-rr where evaluation is not constant (#4100)Andrew Reynolds
Throws warning instead of error if two terms with the same rewritten form evaluate differently, but the evaluation is non-constant. Fixes #4096 and fixes #4089.
2020-03-13Removing a few deprecated options (#4052)Andrew Reynolds
2020-03-13Generalize type rules for strings to sequences (#3987)Andrew Reynolds
Towards theory of sequences.
2020-03-13Fix case of non-constant value for sygus sampling (#4051)Andrew Reynolds
Fixes #4050.
2020-03-12Do not make models for quantified function variables (#4039)Andrew Reynolds
If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.
2020-03-12Ensure legal candidate equalities when using relational triggers (#4035)Andrew Reynolds
2020-03-11Fix double notify in equality engine (#4036)Andrew Reynolds
Fixes #3955. Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context. This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR. A block of code changed indentation in this commit.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback