projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Do not cache operator eliminations in arith (#4542)
[cvc5.git] / test / regress / CMakeLists.txt
2020-05-31 Andres NoetzliDo not cache operator eliminations in arith (#4542) blob | commitdiff | raw
2020-05-26 MartinFix an incorrect limit in conversion from real to float... blob | commitdiff | raw | diff to current
2020-05-23 Andrew ReynoldsRefactor operator elimination in arithmetic (#4519) blob | commitdiff | raw | diff to current
2020-05-22 Andrew Reynolds(proof-new) Add rewrite corresponding to regular expres... blob | commitdiff | raw | diff to current
2020-05-21 Andrew ReynoldsFix missing check for cardinality one in unconstrained... blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsNormal form equality conflicts and uniqueness check... blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsFix parametric datatype instantiation (#4493) blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsDo not eliminate variables that are equal to unevaluata... blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsFix cached free variable identifiers in sygus term... blob | commitdiff | raw | diff to current
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) blob | commitdiff | raw | diff to current
2020-05-19 Andres NoetzliMake SolveEq and PlusCombineLikeTerms idempotent (... blob | commitdiff | raw | diff to current
2020-05-05 Andrew ReynoldsAlways introduce fresh variable for unconstrained APPLY... blob | commitdiff | raw | diff to current
2020-05-02 Andrew ReynoldsMove slow regression to regress3 (#4430) blob | commitdiff | raw | diff to current
2020-04-30 Andrew ReynoldsRemove skolem share involving pre_first_ctn. (#4423) blob | commitdiff | raw | diff to current
2020-04-29 Andrew ReynoldsAvoid circular dependencies for justifying reductions... blob | commitdiff | raw | diff to current
2020-04-28 Andrew ReynoldsUpdate cardinality in strings to unicode standard ... blob | commitdiff | raw | diff to current
2020-04-26 Andrew Reynolds Fix sets cardinality cycle rule (#4392) blob | commitdiff | raw | diff to current
2020-04-22 Andrew ReynoldsEnsure disequality splits are processed as lemmas ... blob | commitdiff | raw | diff to current
2020-04-22 Andres NoetzliReinstantiate support for conjunctions in facts (#4377) blob | commitdiff | raw | diff to current
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910) blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsDo not normalize to representatives for variable equali... blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsAlways assign function values in higher order (#4279) blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsDisable preregistration of instantiations for cegqi... blob | commitdiff | raw | diff to current
2020-04-14 Andrew ReynoldsRemove a few spurious assertions (#4294) blob | commitdiff | raw | diff to current
2020-04-14 Andrew ReynoldsFix dump-unsat-cores-full (#4303) blob | commitdiff | raw | diff to current
2020-04-13 Andrew ReynoldsFix SyGuS define-fun printing from benchmarks coming... blob | commitdiff | raw | diff to current
2020-04-12 Andrew ReynoldsFixes for extended rewriter (#4278) blob | commitdiff | raw | diff to current
2020-04-12 Andrew ReynoldsMove slow nl regression to regress3 (#4276) blob | commitdiff | raw | diff to current
2020-04-11 Andrew ReynoldsEnsure exported sygus solutions match grammar (#4270) blob | commitdiff | raw | diff to current
2020-04-09 Andrew ReynoldsDisable slow sygus regression (#4232) blob | commitdiff | raw | diff to current
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211) blob | commitdiff | raw | diff to current
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) blob | commitdiff | raw | diff to current
2020-04-08 Andrew ReynoldsFix dump models and dump proofs (#4230) blob | commitdiff | raw | diff to current
2020-04-07 Andrew ReynoldsDisable slow regression (#4221) blob | commitdiff | raw | diff to current
2020-04-03 Andrew ReynoldsOnly rewrite lambdas via array representations when... blob | commitdiff | raw | diff to current
2020-04-01 Andrew ReynoldsSupport char smt-lib syntax (#4188) blob | commitdiff | raw | diff to current
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) blob | commitdiff | raw | diff to current
2020-03-30 mudathirmahgoubFrontend support for the choice operator (#4175) blob | commitdiff | raw | diff to current
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... blob | commitdiff | raw | diff to current
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... blob | commitdiff | raw | diff to current
2020-03-26 Andrew ReynoldsDisable slow regression (#4157) blob | commitdiff | raw | diff to current
2020-03-24 yoni206Int2BV fail on demand (#4079) blob | commitdiff | raw | diff to current
2020-03-23 Andrew ReynoldsSimplify auxiliary variable handling in CEGQI (#4141) blob | commitdiff | raw | diff to current
2020-03-22 Andrew ReynoldsSort inference does not handle APPLY_UF when higher... blob | commitdiff | raw | diff to current
2020-03-20 Andrew ReynoldsFix variable shadowing issue in sygus-inference (#4121) blob | commitdiff | raw | diff to current
2020-03-20 Andrew ReynoldsGuard cases of sort inference in quantifier free logics... blob | commitdiff | raw | diff to current
2020-03-20 Andrew ReynoldsDo not assign higher-order representative if function... blob | commitdiff | raw | diff to current
2020-03-19 yoni206Bv2int fail on demand blob | commitdiff | raw | diff to current
2020-03-19 Andres NoetzliOnly apply testConstStringInRegExp to const regexp... blob | commitdiff | raw | diff to current
2020-03-19 Andres NoetzliOnly allow bv2nat/int2bv with BV and integer logic... blob | commitdiff | raw | diff to current
2020-03-19 Andrew ReynoldsFix issue with multiple infinities in CEGQI for LIRA... blob | commitdiff | raw | diff to current
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... blob | commitdiff | raw | diff to current
2020-03-13 Andrew ReynoldsRemove regress for real to int (#4071) blob | commitdiff | raw | diff to current
2020-03-12 Andrew ReynoldsDo not allow quantifiers over real variables in real... blob | commitdiff | raw | diff to current
2020-03-12 Andrew ReynoldsDo not make models for quantified function variables... blob | commitdiff | raw | diff to current
2020-03-12 Aina NiemetzNew C++ API: Remove support for (reset). (#4037) blob | commitdiff | raw | diff to current
2020-03-12 Andrew ReynoldsFix double notify in equality engine (#4036) blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsDo not enable some SMT-COMP specific options by default... blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsGuard against null relevancy condition in SyGuS (#4033) blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsSwitch to Nodes for conjecture generator (#4026) blob | commitdiff | raw | diff to current
2020-03-11 Andres Noetzlireset-assertions: Update TheoryEngine's PropEngine... blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsFix non-parametrized operators in subgoal generation... blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsFix duplicate variable issue in sygus-qe-preproc (... blob | commitdiff | raw | diff to current
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927) blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsFix real to int for parameterized kinds (#4016) blob | commitdiff | raw | diff to current
2020-03-10 Andrew ReynoldsFix sort inference for top-level Boolean variables... blob | commitdiff | raw | diff to current
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) blob | commitdiff | raw | diff to current
2020-03-10 Andrew ReynoldsFix assertion failure in sort inference for Boolean... blob | commitdiff | raw | diff to current
2020-03-10 Andrew ReynoldsDo not set values for non-linear mult terms in collectM... blob | commitdiff | raw | diff to current
2020-03-10 Andrew Reynolds Fix real as int for incremental (#3979) blob | commitdiff | raw | diff to current
2020-03-10 Andrew ReynoldsDo not traverse quantifiers in nl ext purify (#3982) blob | commitdiff | raw | diff to current
2020-03-10 makaimannEnhancement: make the bool-to-bv pass more robust and... blob | commitdiff | raw | diff to current
2020-03-10 Andrew ReynoldsEnsure standard miniscoping is applied before aggressiv... blob | commitdiff | raw | diff to current
2020-03-09 Andrew ReynoldsFix type issue in arith rewrite equality (#3972) blob | commitdiff | raw | diff to current
2020-03-09 Andres NoetzliMake registration of unit clauses more robust (#3965) blob | commitdiff | raw | diff to current
2020-03-09 Andrew ReynoldsRewrite again full for DIV rewrite (#3945) blob | commitdiff | raw | diff to current
2020-03-08 Ying ShengExplicit end marker for models printed in the CVC langu... blob | commitdiff | raw | diff to current
2020-03-06 Andrew ReynoldsSupport default sygus grammar construction for sets... blob | commitdiff | raw | diff to current
2020-03-05 Andrew ReynoldsFix issues with real to int (#3918) blob | commitdiff | raw | diff to current
2020-02-29 Andrew Reynolds Throw warning instead of error for non-constant values... blob | commitdiff | raw | diff to current
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) blob | commitdiff | raw | diff to current
2020-02-29 Andrew ReynoldsFix assertion related to assignability in the model... blob | commitdiff | raw | diff to current
2020-02-29 Andrew ReynoldsReplace conditional rewrite pass in quantifiers with... blob | commitdiff | raw | diff to current
2020-02-27 Andrew ReynoldsFix large models for strings (#3835) blob | commitdiff | raw | diff to current
2020-02-27 Andrew ReynoldsAdd support for is_digit and regular expression differe... blob | commitdiff | raw | diff to current
2020-02-27 Andrew ReynoldsDisable regression that times out on debug (#3833) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsUse side effect utility for non-linear lemmas (#3780) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsUse default consts when not using any const during... blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsFix node arity issue in reduction of int2bv (#3777) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsSupport for witnessing choice in models (#3781) blob | commitdiff | raw | diff to current
2020-02-25 yoni206bv_to_int preprocessing pass blob | commitdiff | raw | diff to current
2020-02-24 Andres NoetzliMake lambda rewriter more robust (#3806) blob | commitdiff | raw | diff to current
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741) blob | commitdiff | raw | diff to current
2020-02-21 Andrew ReynoldsSimple changes towards unicode string standard (#3791) blob | commitdiff | raw | diff to current
2020-02-19 Andrew ReynoldsDelay enumerative instantiation if theory engine does... blob | commitdiff | raw | diff to current
2020-02-17 Andrew Reynolds Fix soundness bug in reduction of integer div/mod... blob | commitdiff | raw | diff to current
2020-02-16 Andrew ReynoldsDisable regression (#3761) blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) blob | commitdiff | raw | diff to current
2020-02-12 Andrew ReynoldsEnsure ext rewrites for associative ops dont throw... blob | commitdiff | raw | diff to current
next