projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix antecedent loop. Whoops
[cvc5.git] / src /
2020-03-16 Alex OzdemirFix antecedent loop. Whoops tree | commitdiff
2020-03-16 Alex OzdemirOnly save farkas+tightening proofs. Error on holes tree | commitdiff
2020-03-16 Alex OzdemirExpand the definition of a "simple" farkas proof. tree | commitdiff
2020-03-16 Aina NiemetzDecisionEngine: Use single unique pointer for ITE strat... tree | commitdiff
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... tree | commitdiff
2020-03-16 Andrew ReynoldsHandle cases in --sygus-rr where evaluation is not... tree | commitdiff
2020-03-13 Andrew ReynoldsRemoving a few deprecated options (#4052) tree | commitdiff
2020-03-13 Andrew ReynoldsGeneralize type rules for strings to sequences (#3987) tree | commitdiff
2020-03-13 Andrew ReynoldsFix case of non-constant value for sygus sampling ... tree | commitdiff
2020-03-12 Andrew ReynoldsConvert most instances of dataypes in parsers to the... tree | commitdiff
2020-03-12 Andrew ReynoldsDo not allow quantifiers over real variables in real... tree | commitdiff
2020-03-12 Andrew ReynoldsRemove local theory extension option (#4048) tree | commitdiff
2020-03-12 Andrew ReynoldsDo not make models for quantified function variables... tree | commitdiff
2020-03-12 Aina NiemetzNew C++ API: Remove support for (reset). (#4037) tree | commitdiff
2020-03-12 Andrew ReynoldsEnsure legal candidate equalities when using relational... tree | commitdiff
2020-03-12 Andrew ReynoldsFix double notify in equality engine (#4036) tree | commitdiff
2020-03-12 Aina NiemetzHide options for and related to the BV abstraction... tree | commitdiff
2020-03-12 Andrew ReynoldsSimplifications to the Datatypes API (#4040) tree | commitdiff
2020-03-12 makaimannAdd automatic Cython binding installation (#3933) tree | commitdiff
2020-03-11 Andrew ReynoldsDo not enable some SMT-COMP specific options by default... tree | commitdiff
2020-03-11 Andrew ReynoldsGuard against null relevancy condition in SyGuS (#4033) tree | commitdiff
2020-03-11 Andrew ReynoldsAdd missing datatype functions to new API (#3930) tree | commitdiff
2020-03-11 Andrew ReynoldsSwitch to Nodes for conjecture generator (#4026) tree | commitdiff
2020-03-11 Andres Noetzlireset-assertions: Update TheoryEngine's PropEngine... tree | commitdiff
2020-03-11 Andrew ReynoldsRemove experimental symmetry breaker (#4005) tree | commitdiff
2020-03-11 Andrew ReynoldsFix non-parametrized operators in subgoal generation... tree | commitdiff
2020-03-11 Andrew ReynoldsRemove partial instantiation for local theory extension... tree | commitdiff
2020-03-11 Andrew ReynoldsFix (#4017) tree | commitdiff
2020-03-11 Andrew ReynoldsFix duplicate variable issue in sygus-qe-preproc (... tree | commitdiff
2020-03-11 Andres NoetzliIntroduce tables in the rewriter (#3742) tree | commitdiff
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927) tree | commitdiff
2020-03-11 Aina Niemetzbv-gauss-elim: Fix handling of inconsistent case. ... tree | commitdiff
2020-03-11 Andrew ReynoldsFix real to int for parameterized kinds (#4016) tree | commitdiff
2020-03-10 Andrew ReynoldsFix sort inference for top-level Boolean variables... tree | commitdiff
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) tree | commitdiff
2020-03-10 Andrew ReynoldsLogic exception instead of assertion failure for instan... tree | commitdiff
2020-03-10 Andrew ReynoldsRemove assertion in resolution bound inferences (#3980) tree | commitdiff
2020-03-10 Andrew ReynoldsConsolidate options that disable produceModels (#3973) tree | commitdiff
2020-03-10 Andrew ReynoldsFix assertion failure in sort inference for Boolean... tree | commitdiff
2020-03-10 Aina NiemetzFix -Wshadow warnings in sygus_grammar_cons.cpp. (... tree | commitdiff
2020-03-10 Andrew ReynoldsDo not set values for non-linear mult terms in collectM... tree | commitdiff
2020-03-10 Andrew Reynolds Fix real as int for incremental (#3979) tree | commitdiff
2020-03-10 Andrew ReynoldsDo not traverse quantifiers in nl ext purify (#3982) tree | commitdiff
2020-03-10 Andrew ReynoldsOnly register sygus terms to unfold if option is set... tree | commitdiff
2020-03-10 Alex OzdemirDocument bv-to-bool recursion (#3848) tree | commitdiff
2020-03-10 makaimannEnhancement: make the bool-to-bv pass more robust and... tree | commitdiff
2020-03-10 Andrew ReynoldsRename sygus option name (#3977) tree | commitdiff
2020-03-10 Andrew ReynoldsRemove instantiation propagator infrastructure (#3975) tree | commitdiff
2020-03-10 Andrew ReynoldsEnsure standard miniscoping is applied before aggressiv... tree | commitdiff
2020-03-09 Andrew ReynoldsEliminate spurious assertion (#3976) tree | commitdiff
2020-03-09 Aina NiemetzDecisionEngine: Use unique_ptr for enabled strategies... tree | commitdiff
2020-03-09 Andrew ReynoldsFix type issue in arith rewrite equality (#3972) tree | commitdiff
2020-03-09 Andres NoetzliMake registration of unit clauses more robust (#3965) tree | commitdiff
2020-03-09 Andrew ReynoldsClean up more uses of ExprManager in parsers (#3932) tree | commitdiff
2020-03-09 Andrew ReynoldsConvert more uses of strings to words (#3921) tree | commitdiff
2020-03-09 Andrew ReynoldsFixes for bounds on transcendental functions (#3832) tree | commitdiff
2020-03-09 Andrew ReynoldsRewrite again full for DIV rewrite (#3945) tree | commitdiff
2020-03-08 Ying ShengExplicit end marker for models printed in the CVC langu... tree | commitdiff
2020-03-06 Andrew ReynoldsMinor refactor for theory of sets (#3924) tree | commitdiff
2020-03-06 Andrew ReynoldsSimplify DatatypeDeclarationCommand command (#3928) tree | commitdiff
2020-03-06 Andrew ReynoldsRemove tester name from APIs (#3929) tree | commitdiff
2020-03-06 Andrew ReynoldsMake sygus datatype building independent of parser... tree | commitdiff
2020-03-06 Andrew ReynoldsSupport default sygus grammar construction for sets... tree | commitdiff
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) tree | commitdiff
2020-03-05 Alex OzdemirAdd a new arith constraint proof rule: IntTightenAP... tree | commitdiff
2020-03-05 Alex OzdemirRevert "Add a new arith constraint proof rule: IntTight... tree | commitdiff
2020-03-05 Andres NoetzliAdd a new arith constraint proof rule: IntTightenAP... tree | commitdiff
2020-03-05 Andrew ReynoldsMigrate a majority of the functionality in parsers... tree | commitdiff
2020-03-05 Aina NiemetzMove ownership of DecisionEngine into PropEngine. ... tree | commitdiff
2020-03-05 Aina NiemetzRevert "Move ownership of DecisionEngine into PropEngin... tree | commitdiff
2020-03-05 Andrew ReynoldsMove ownership of DecisionEngine into PropEngine. ... tree | commitdiff
2020-03-05 Andrew ReynoldsFix issues with real to int (#3918) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-03-03 mudathirmahgoubRefactoring and cleaning the type enumerator for sets... tree | commitdiff
2020-03-03 Andrew ReynoldsStandardize the interface for SMT engine subsolvers... tree | commitdiff
2020-03-03 Andres NoetzliFix `TheorySetsPrive::eqNotifyPostMerge()` (#3901) tree | commitdiff
2020-03-03 Mathias PreinerFix variable shadowing bug in sets. (#3898) tree | commitdiff
2020-03-02 Andrew Reynolds Split collect model info by types in strings (#3847) tree | commitdiff
2020-02-29 Andrew ReynoldsConvert more uses of string to word (#3834) tree | commitdiff
2020-02-29 Andrew Reynolds Throw warning instead of error for non-constant values... tree | commitdiff
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) tree | commitdiff
2020-02-29 Aina NiemetzpropEngine: Reorder class declaration according to... tree | commitdiff
2020-02-29 Andrew ReynoldsFix assertion related to assignability in the model... tree | commitdiff
2020-02-29 Andrew ReynoldsReplace conditional rewrite pass in quantifiers with... tree | commitdiff
2020-02-28 Andrew ReynoldsUse enum for quantifiers rewrite steps (#3840) tree | commitdiff
2020-02-27 Andrew ReynoldsRefactor operator applications in the parser (#3831) tree | commitdiff
2020-02-27 Haniel BarbosaChanging TPTP parser to accomodate new API (#3837) tree | commitdiff
2020-02-27 Andrew ReynoldsUpdate purifySygusGTerm to the new API (#3830) tree | commitdiff
2020-02-27 Andrew ReynoldsFix large models for strings (#3835) tree | commitdiff
2020-02-27 Andres NoetzliFix -Wshadow warnings in common headers (#3826) tree | commitdiff
2020-02-27 Andrew ReynoldsAdd support for is_digit and regular expression differe... tree | commitdiff
2020-02-27 Andrew ReynoldsMove fix for vacuous sygus types out of the parser... tree | commitdiff
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817) tree | commitdiff
2020-02-27 Andrew ReynoldsSome initial work on using words (#3819) tree | commitdiff
2020-02-26 Andrew ReynoldsInfrastructure for tautological literals in nonlinear... tree | commitdiff
2020-02-26 Andrew ReynoldsUse side effect utility for non-linear lemmas (#3780) tree | commitdiff
2020-02-26 Andrew ReynoldsFix regression (#3827) tree | commitdiff
2020-02-26 Andrew ReynoldsMore fixes for printing sygus commands (#3812) tree | commitdiff
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437) tree | commitdiff
2020-02-26 Andrew ReynoldsRefactor type ascriptions in the parser (#3825) tree | commitdiff
next