summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2018-07-04Merge branch 'sygusComp2018-2' into replaceSubstitutereplaceSubstituteAndres Noetzli
2018-06-27Fixajreynol
2018-06-27Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2ajreynol
2018-06-26sygusComp2018: Add evaluator (#2090)Andres Noetzli
This commit adds the Evaluator class that can be used to quickly evaluate terms under a given substitution without going through the rewriter. This has been shown to lead to significant performance improvements on SyGuS PBE problems with a large number of inputs because candidate solutions are evaluated on those inputs. With this commit, the evaluator only gets called from the SyGuS solver but there are potentially other places in the code that could profit from it.
2018-06-26 Disable uf symmetry breaker in incremental mode (#2091)Andrew Reynolds
2018-06-26Fix assertion for relational triggers (#2096)Andrew Reynolds
2018-06-26 Do not dagify printing over binders (#2093)Andrew Reynolds
2018-06-26Remove unnecessary code in register quantifier internal (#2092)Andrew Reynolds
2018-06-26Formatajreynol
2018-06-26Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2ajreynol
2018-06-25Minor improvements in SMT2 and CVC printers (#2089)Andres Noetzli
This commit adds support for string concatenation, charat, and length operators in the CVC printer and support for re.nostr, re.allchar, and insert into a set in the SMT2 printer.
2018-06-25Update copyright year in configuration.cpp:copyright().Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-25Remove parentheses for prefix ops without args (#2082)Andres Noetzli
In the CVC printer, function definitions without arguments are printed like constants but when actually using that function we were printing in the form of `x()`. For example: ``` (set-logic QF_BV) (define-fun x1480 () Bool true) (define-fun x2859 () Bool true) (define-fun x2387 () Bool x2859) (check-sat) ``` Was dumped as: ``` OPTION "incremental" false; OPTION "logic" "QF_BV"; x1480 : BOOLEAN = TRUE; x2859 : BOOLEAN = TRUE; x2387 : BOOLEAN = x2859(); ``` This commit removes these parentheses when prefix functions with zero arguments are printed, so the example above becomes: ``` OPTION "incremental" false; OPTION "logic" "QF_BV"; x1480 : BOOLEAN = TRUE; x2859 : BOOLEAN = TRUE; x2387 : BOOLEAN = x2859(); ```
2018-06-21final fixAndres Noetzli
2018-06-20Fix warnings and enable -Wnon-virtual-dtor warning (#2079)Andres Noetzli
This commit fixes warnings for an unused variable, comparison of two different types and add virtual destructors to classes that were previously missing them. It also enables the -Wnon-virtual-dtor warning which warns about any class definition with virtual methods that does not have a virtual destructor (except if the destructor is protected). This flag is supported by both clang and GCC and not enabled by default.
2018-06-20Resolve CVC4_USE_SYMFPU in headers at config-time (#2077)Andres Noetzli
As described in issue #2013, we had `#ifdef CVC4_USE_SYMFPU` conditions in floatingpoint.h, which was problematic when installing the header files because the definition of `CVC4_USE_SYMFPU` was a compile-flag and simply including the header files in another project would be missing that definition. This commit moves floatingpoint.h to a template file floatingpoint.h.in and substitutes the value of `CVC4_USE_SYMFPU` at configure-time when generating floatingpoint.h (this is the same solution that integer.h and rational.h use). I have tested the fix with the examples provided in #2013 and they work.
2018-06-20Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2ajreynol
2018-06-19fixesAndres Noetzli
2018-06-19Infer substitutions in str.contains rewriterAndres Noetzli
2018-06-19Minor to PBE solution.ajreynol
2018-06-19ITE strategy first.ajreynol
2018-06-19Option to disable multi-enumerator fairnessajreynol
2018-06-19Update option.ajreynol
2018-06-19Optionajreynol
2018-06-19Cleanajreynol
2018-06-19Fix, empty-subs rewrite.ajreynol
2018-06-19More replace rewrites.ajreynol
2018-06-19Fix commentajreynol
2018-06-18A few strings rewrites.ajreynol
2018-06-18Fix (disabled)ajreynol
2018-06-18Constant repair abort option, update script.ajreynol
2018-06-18Allow multiple strategies if one immediately fails.ajreynol
2018-06-18Reorg in prep for multiple strategies.ajreynol
2018-06-18More infrastructure to strats.ajreynol
2018-06-18Merge pull request #12 from 4tXJ7f/replaceReplaceAndrew Reynolds
2018-06-18fix commentreplaceReplaceAndres Noetzli
2018-06-18canConstructKind infrastructure.ajreynol
2018-06-18Merge branch 'sygusComp2018-2' into replaceReplaceAndres Noetzli
2018-06-18Generalize to replace in containsAndres Noetzli
2018-06-17Merge pull request #10 from 4tXJ7f/replSubstAndrew Reynolds
2018-06-17address commentreplSubstAndres Noetzli
2018-06-16Rewrite for (str.replace x (str.replace y z w) u)Andres Noetzli
This commit adds the following rewrite: (str.replace x (str.replace y z w) u) --> x if (str.contains x y) = false and (str.contains x w) = false Reasoning: (str.contains x y) checks that x does not contain y if the inner replacement does not change y. (str.contains x w) checks that if the inner replacement changes anything in y, the w makes it impossible for it to occur in x.
2018-06-16Evaluator: support and/or, contains, prefix/suffixeval6Andres Noetzli
2018-06-16Infrastructure, reorg relevancy conditions.ajreynol
2018-06-15Rewrite subtring length if used in replacementAndres Noetzli
In cases such as (str.replace x (str.++ ... (str.substr y i j)) z), we can restrict j to len(x) + 1 - len(...) if j > len(x) + 1. Because if the string to be replaced is longer than x, then it does not matter how much longer it is, the result is always x. Thus, it is fine to only look at the prefix of length len(x) + 1 - len(...).
2018-06-15Formatajreynol
2018-06-15All-constant symmetry breaking.ajreynol
2018-06-15isconstant predicate.ajreynol
2018-06-15Merge pull request #9 from 4tXJ7f/lengthPreserveAndrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback