cvc5.git
2020-03-11 Andrew ReynoldsDo not enable some SMT-COMP specific options by default...
2020-03-11 Andrew ReynoldsGuard against null relevancy condition in SyGuS (#4033)
2020-03-11 Andrew ReynoldsAdd missing datatype functions to new API (#3930)
2020-03-11 Andrew ReynoldsSwitch to Nodes for conjecture generator (#4026)
2020-03-11 Andres Noetzlireset-assertions: Update TheoryEngine's PropEngine...
2020-03-11 Andrew ReynoldsRemove experimental symmetry breaker (#4005)
2020-03-11 Andrew ReynoldsFix non-parametrized operators in subgoal generation...
2020-03-11 Andrew ReynoldsRemove partial instantiation for local theory extension...
2020-03-11 Andrew ReynoldsFix (#4017)
2020-03-11 Andrew ReynoldsFix duplicate variable issue in sygus-qe-preproc (...
2020-03-11 Andres NoetzliIntroduce tables in the rewriter (#3742)
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927)
2020-03-11 Aina Niemetzbv-gauss-elim: Fix handling of inconsistent case. ...
2020-03-11 Andrew ReynoldsFix real to int for parameterized kinds (#4016)
2020-03-10 Andrew ReynoldsFix options for regression: --sort-inference is incompa...
2020-03-10 Andrew ReynoldsFix sort inference for top-level Boolean variables...
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988)
2020-03-10 Andrew ReynoldsLogic exception instead of assertion failure for instan...
2020-03-10 Mathias PreinerUpdate bug report template
2020-03-10 Andrew ReynoldsRemove assertion in resolution bound inferences (#3980)
2020-03-10 Aina NiemetzUse fixed-width types in test/unit/context/contest_mm_b...
2020-03-10 Aina NiemetzFix -Wshadow warning in test/unit/context/context_mm_bl...
2020-03-10 Andrew ReynoldsConsolidate options that disable produceModels (#3973)
2020-03-10 Andrew ReynoldsFix assertion failure in sort inference for Boolean...
2020-03-10 Aina NiemetzFix -Wshadow warnings in sygus_grammar_cons.cpp. (...
2020-03-10 Andrew ReynoldsDo not set values for non-linear mult terms in collectM...
2020-03-10 Andrew Reynolds Fix real as int for incremental (#3979)
2020-03-10 Andrew ReynoldsDo not traverse quantifiers in nl ext purify (#3982)
2020-03-10 Andrew ReynoldsOnly register sygus terms to unfold if option is set...
2020-03-10 Alex OzdemirDocument bv-to-bool recursion (#3848)
2020-03-10 makaimannEnhancement: make the bool-to-bv pass more robust and...
2020-03-10 Andrew ReynoldsRename sygus option name (#3977)
2020-03-10 Andrew ReynoldsRemove instantiation propagator infrastructure (#3975)
2020-03-10 Andrew ReynoldsEnsure standard miniscoping is applied before aggressiv...
2020-03-09 Andrew ReynoldsEliminate spurious assertion (#3976)
2020-03-09 Aina NiemetzDecisionEngine: Use unique_ptr for enabled strategies...
2020-03-09 Andrew ReynoldsFix type issue in arith rewrite equality (#3972)
2020-03-09 Andres NoetzliMake registration of unit clauses more robust (#3965)
2020-03-09 Andres NoetzliIncrease stack size for Windows builds to 100 MB (...
2020-03-09 Andrew ReynoldsClean up more uses of ExprManager in parsers (#3932)
2020-03-09 Andrew ReynoldsConvert more uses of strings to words (#3921)
2020-03-09 Andres NoetzliFix quoting of options on Travis (#3981)
2020-03-09 Andrew ReynoldsFixes for bounds on transcendental functions (#3832)
2020-03-09 Andrew ReynoldsRewrite again full for DIV rewrite (#3945)
2020-03-08 Ying ShengExplicit end marker for models printed in the CVC langu...
2020-03-06 Andrew ReynoldsMinor refactor for theory of sets (#3924)
2020-03-06 Andrew ReynoldsSimplify DatatypeDeclarationCommand command (#3928)
2020-03-06 Andrew ReynoldsRemove tester name from APIs (#3929)
2020-03-06 Andres NoetzliIgnore model check warning in regression test (#3926)
2020-03-06 Andrew ReynoldsMake sygus datatype building independent of parser...
2020-03-06 Andrew ReynoldsSupport default sygus grammar construction for sets...
2020-03-06 Andres NoetzliMake output of regression script more readable (#3911)
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919)
2020-03-05 Alex OzdemirAdd a new arith constraint proof rule: IntTightenAP...
2020-03-05 Alex OzdemirRevert "Add a new arith constraint proof rule: IntTight...
2020-03-05 Andres NoetzliAdd a new arith constraint proof rule: IntTightenAP...
2020-03-05 Andrew ReynoldsMigrate a majority of the functionality in parsers...
2020-03-05 Aina NiemetzMove ownership of DecisionEngine into PropEngine. ...
2020-03-05 Aina NiemetzRevert "Move ownership of DecisionEngine into PropEngin...
2020-03-05 Andrew ReynoldsMove ownership of DecisionEngine into PropEngine. ...
2020-03-05 Andrew ReynoldsFix issues with real to int (#3918)
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909)
2020-03-03 mudathirmahgoubRefactoring and cleaning the type enumerator for sets...
2020-03-03 Andrew ReynoldsStandardize the interface for SMT engine subsolvers...
2020-03-03 Andres NoetzliFix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)
2020-03-03 Mathias PreinerFix variable shadowing bug in sets. (#3898)
2020-03-02 Andrew Reynolds Split collect model info by types in strings (#3847)
2020-02-29 Andrew ReynoldsConvert more uses of string to word (#3834)
2020-02-29 Andrew Reynolds Throw warning instead of error for non-constant values...
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829)
2020-02-29 Aina NiemetzpropEngine: Reorder class declaration according to...
2020-02-29 Andrew ReynoldsFix assertion related to assignability in the model...
2020-02-29 Andrew ReynoldsReplace conditional rewrite pass in quantifiers with...
2020-02-28 Andrew ReynoldsUse enum for quantifiers rewrite steps (#3840)
2020-02-27 Andrew ReynoldsRefactor operator applications in the parser (#3831)
2020-02-27 Haniel BarbosaChanging TPTP parser to accomodate new API (#3837)
2020-02-27 Andrew ReynoldsUpdate purifySygusGTerm to the new API (#3830)
2020-02-27 Andrew ReynoldsFix large models for strings (#3835)
2020-02-27 Andres NoetzliFix -Wshadow warnings in common headers (#3826)
2020-02-27 Andrew ReynoldsAdd support for is_digit and regular expression differe...
2020-02-27 Andrew ReynoldsDisable regression that times out on debug (#3833)
2020-02-27 Andrew ReynoldsMove fix for vacuous sygus types out of the parser...
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817)
2020-02-27 Andrew ReynoldsSome initial work on using words (#3819)
2020-02-26 Andrew ReynoldsInfrastructure for tautological literals in nonlinear...
2020-02-26 Andrew ReynoldsUse side effect utility for non-linear lemmas (#3780)
2020-02-26 Andrew ReynoldsFix regression (#3827)
2020-02-26 Andrew ReynoldsMore fixes for printing sygus commands (#3812)
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437)
2020-02-26 Andrew ReynoldsRefactor type ascriptions in the parser (#3825)
2020-02-26 Andrew ReynoldsMinor improvement to ParseOp (#3808)
2020-02-26 Andrew ReynoldsUse default consts when not using any const during...
2020-02-26 Andrew ReynoldsFix node arity issue in reduction of int2bv (#3777)
2020-02-26 Andrew ReynoldsMove equivalence class info to its own file in strings...
2020-02-26 Andrew ReynoldsSupport for witnessing choice in models (#3781)
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821)
2020-02-26 Andrew ReynoldsMinor cleaning of smt2 parser (#3823)
2020-02-26 Andrew ReynoldsEmbed mkAssociative utilities within the API. (#3801)
2020-02-25 mudathirmahgoubSets & Relations Java example (#3816)
2020-02-25 mudathirmahgoubSets & Relations Java example (#3816)
next