summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-07[SMT2 Parser] Move code of `rewriterulesCommand` (#3334)Andres Noetzli
This commit moves the code in `rewriterulesCommand` in the SMT2 parser to the `Smt2` class. Additionally, it creates a `boundVarList` rule to reduce code duplication.
2019-10-06Fix typo in regression (#3359)Andrew Reynolds
2019-10-06Fix str to int reduction (#3358)Andrew Reynolds
This fixes a corner case of the str-to-int reduction for the case where the argument is the empty string. This fixes #3357.
2019-10-04Avoid duplicate lemmas in datatypes (#3310)Andrew Reynolds
We previously were sending e.g. dt.size >= 0 lemmas when size terms are pre-registered, which can happen multiple times in a user context. This ensures we cache whether a lemma is sent in a user-context dependent way in the datatypes solver. This ensures we don't send the same lemma twice for dt.size >= 0 lemmas.
2019-10-03Disable proofs for unsupported logics (#3327)yoni206
This commit makes CVC4 complain if the user asked for proofs for an unsupported logic (in this contest, ALL is considered unsupported). Changes in the regression script are introduced as well, in order to only request proofs for regressions in supported logics.
2019-10-03Travis: Reenable building and running of examples. (#3351)Aina Niemetz
2019-10-03Add missing type definitions to CDHashMap iterator (#3330)Andres Noetzli
Our `CDMapBlack` test failed to compile with newer versions of libstdc++ because they require the `value_type` to be defined for the iterator (accessed via `std::iterator_traits`). Due to the implementation of `std::iterator_traits`, we also need to define `iterator_category`, `difference_type`, `pointer`, and `reference`.
2019-10-03[SMT2 Parser] Move code of `sygusCommand` (#3335)Andres Noetzli
This commit moves the code in `sygusCommand` in the SMT2 parser to the `Smt2` class. The original code was pushing and popping the current scope inline. This commit adds a class `SynthFunFactory` that takes care of that upon creation and destruction.
2019-10-02Fix compiler warning. (#3348)Aina Niemetz
2019-10-02[SMT-COMP] Remove --unconstrained-simp for incremental QF_LIA (#3333)Andres Noetzli
Fixes #3058. Commit a7c4cd3ecacb1e484a076edde0274c282bb43ffb changed CVC4's behavior to emit an error when `--unconstrained-simp` is used with `--incremental`. Before, we were silently disabling it. For some reason, we had that option enabled for the incremental QF_LIA track of SMT-COMP, so CVC4 failed on those benchmarks. This commit changes the corresponding competition script to not use the option.
2019-09-30Trivial solve method for single invocation sygus (#3328)Andrew Reynolds
This short circuits CEGQI when the conjecture is solvable by simple equality reasoning. It adds two examples where we previously would have fallen back on enumeration due to not having an instantiation technique for strings, despite the conjectures being trivially solvable.
2019-09-29Add rewrite for splitting equalities (#2957)Andres Noetzli
2019-09-29Add help for sygus 2.0 (#3318)Andrew Reynolds
2019-09-29Avoid cases of empty sygus grammars (#3301)Andrew Reynolds
2019-09-29Fail single invocation techniques when utility inference fails. (#3322)Andrew Reynolds
2019-09-28Introduce template classes for simple type rules (#2835)Andres Noetzli
This commit introduces two template classes `SimpleTypeRule` and `SimpleTypeRuleVar` to help define simple type rules without writing lots of redundant code. The main advantages of this approach are: - Less code - More consistent error reporting - Easier to extend type checking with other functionality (e.g. getting the type of a symbol)
2019-09-27Support smt2 language "match" term (#3258)Andrew Reynolds
2019-09-27Fix case of disjunctive conclusion in strings (#3254)Andrew Reynolds
2019-09-27Make substitution index context-independent (#2474)Andres Noetzli
When we do solving in incremental mode, we store substitutions at a special index in our list of assertions. Previously, we used a context-dependent variable for that. However, this is not needed since the list of assertions just consists of the assertions currently being processed, which are independent of the assertions seen so far. This commit changes the index to be an ordinary integer and moves it to the AssertionPipeline. Additionally, it abstracts access to the index in preparation for splitting AssertionPipeline into three vectors (see issue #2473).
2019-09-26CVC print support for recoverable failure (#3323)Andrew Reynolds
2019-09-25 Fix off by one error in strings flat form explanation (#3273)Andrew Reynolds
Fixes #3272. This was caused by not explaining the last equal component in a flat form inference. For example, if `x=y`, we may infer `z=""` from `u++x++z=u++y` since the 1st and 2nd components of these strings are equal. However, we would not add the explanation of `x=y` due to an off-by-one error. Notice that this code is very rarely used (the code for F_EndpointEmp is not covered by our regressions). This is since length elaboration should catch conflicting cases like above, where `len(u++x++z)!=len(u++y)` if `x=y` and `z!=""` and thus `u++x++z != u++y`. #3272 happened to catch a rare case where it is applied. This is likely due to theory combination not propagating an equality prior to running a full effort call to strings check, which is unexpected but not impossible.
2019-09-25Add isParameterized function to Expr (#3303)Andrew Reynolds
2019-09-25Use separate CMake project for CVC4 examples. (#3196)Mathias Preiner
2019-09-25Add Windows cross-compiling instructions to INSTALL.md. (#3226)Mathias Preiner
2019-09-25Fix printing of instantiation patterns (#3305)Andrew Reynolds
2019-09-24Return choice functions for approximate values in get-value (#3304)Andrew Reynolds
2019-09-19Support context-(in)dependent decision strategies. (#3281)Andrew Reynolds
2019-09-18Add support for creating constant arrays to the new C++ API (#3296)makaimann
* Add support for constant arrays to new C++ API * Fix macro usage in unit test * Add not null check * Add test for null term * Formatting
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-18Add run script for next SMT-COMP (#3298)Andres Noetzli
2019-09-18Minor cleaning (#3295)Andrew Reynolds
2019-09-17 Encapsulate relevant domain (#3293)Andrew Reynolds
2019-09-16Avoid computing cardinality when constructing models (#3268)Andrew Reynolds
2019-09-16Remove parameterized check (#3290)Andrew Reynolds
2019-09-16Fix spurious meta-info in regression (#3294)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-09-16Move specific attributes out of term util (#3279)Andrew Reynolds
2019-09-16Sygus type info class (#3187)Andrew Reynolds
2019-09-16 Fix HO model construction for functions having Boolean arguments (#3158)Andrew Reynolds
2019-09-16Move virtual term substitution utilities to own file and document (#3278)Andrew Reynolds
2019-09-16Return RecoverableModalException when model is not available. (#3283)Andrew Reynolds
2019-09-16Fix compiler warning in options.cpp. (#3284)Aina Niemetz
2019-09-16Adding new scripts for CASC/TPTP (#3291)Haniel Barbosa
2019-09-16Initialize fields in sets inference manager (#3289)Andrew Reynolds
2019-09-16parser: Improve error message for unrecognized input file format. (#3285)Aina Niemetz
2019-09-13Disallow let in sygus grammars, check for free variables in sygus ↵Andrew Reynolds
constructors (#3259)
2019-09-13Move higher-order matching predicate (#3280)Andrew Reynolds
2019-09-13Split, refactor and document the theory of sets (#3085)Andrew Reynolds
2019-09-12 Rename UF with cardinality extension (#3241)Andrew Reynolds
2019-09-12Update to standard implementation of contains term (#3270)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback