cvc5.git
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)
2020-02-25 yoni206remove redundant includes (#3815)
2020-02-25 yoni206bv_to_int preprocessing pass
2020-02-24 Andrew ReynoldsFixes for quantifiers documentation (#3811)
2020-02-24 Andrew ReynoldsUtilities for words (#3797)
2020-02-24 Andrew ReynoldsConvert parser input interface to api::Term (#3809)
2020-02-24 Abdalrhman... Fix bugs related to printing Sygus commands (#3804)
2020-02-24 Andrew ReynoldsAdd missing functions to new C++ API (#3769)
2020-02-24 Andres NoetzliMake lambda rewriter more robust (#3806)
2020-02-23 Andrew ReynoldsMinor refactoring of equality notifications (#3798)
2020-02-22 Alex OzdemirRIP th_lra.plf (#3796)
2020-02-22 Andrew Reynolds Move check memberships to reg exp solver (#3793)
2020-02-22 Andrew ReynoldsMove cardinality inference scheme to base solver in...
2020-02-22 makaimannDump boolean propagations and conflicts for decision...
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741)
2020-02-21 Aina NiemetzNew C++ API: Remove TOTAL kinds. (#3794)
2020-02-21 Andrew ReynoldsSimple changes towards unicode string standard (#3791)
2020-02-21 Andrew V. JonesAdding checks to the validation of 'bv-sat-solver'...
2020-02-21 Andrew ReynoldsSplit extended functions solver in strings (#3768)
2020-02-21 Alex OzdemirRemove IntReal tightening axioms from th_lira.plf ...
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767)
2020-02-20 Andres NoetzliRemove unused code (#3782)
2020-02-20 Andrew ReynoldsMinor removals (#3786)
2020-02-20 Andres NoetzliRemove parser from bindings (#3779)
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource...
2020-02-19 Andrew ReynoldsFix symmetry breaking for multiple sygus types (#3775)
2020-02-19 makaimannAdd Python bindings using Cython -- see below for more...
2020-02-19 Andrew ReynoldsDelay enumerative instantiation if theory engine does...
2020-02-19 Andrew ReynoldsChange Record to shared_ptr (#3778)
2020-02-19 Andrew ReynoldsFix approximate bounds for transcendental functions...
2020-02-19 makaimannChange datatype selector/constructor/tester to terms...
2020-02-18 Andrew ReynoldsAdd missing kinds for the new API (#3757)
2020-02-17 Andrew ReynoldsOption to limit the number of rounds of enumerative...
2020-02-17 Andrew Reynolds Fix soundness bug in reduction of integer div/mod...
2020-02-17 Haniel BarbosaUsing ParseOp in TPTP (#3764)
2020-02-17 Abdalrhman... Support dumping Sygus commands. (#3763)
2020-02-16 Andrew ReynoldsFix simple issue with cache (#3762)
2020-02-16 Andrew ReynoldsAdd temporary global API conversion utilities. (#3759)
2020-02-16 Andres NoetzliActivate reverse variant of F-Split inference (#3745)
2020-02-16 Andrew ReynoldsDisable regression (#3761)
2020-02-15 Andrew ReynoldsMove proxy variables to InferenceManager in strings...
next