projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add a new arith constraint proof rule: IntTightenAP (#3818)
[cvc5.git] / src /
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
2020-02-26 Andrew ReynoldsMinor improvement to ParseOp (#3808) tree | commitdiff
2020-02-26 Andrew ReynoldsUse default consts when not using any const during... tree | commitdiff
2020-02-26 Andrew ReynoldsFix node arity issue in reduction of int2bv (#3777) tree | commitdiff
2020-02-26 Andrew ReynoldsMove equivalence class info to its own file in strings... tree | commitdiff
2020-02-26 Andrew ReynoldsSupport for witnessing choice in models (#3781) tree | commitdiff
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821) tree | commitdiff
2020-02-26 Andrew ReynoldsMinor cleaning of smt2 parser (#3823) tree | commitdiff
2020-02-26 Andrew ReynoldsEmbed mkAssociative utilities within the API. (#3801) tree | commitdiff
2020-02-25 yoni206remove redundant includes (#3815) tree | commitdiff
2020-02-25 yoni206bv_to_int preprocessing pass tree | commitdiff
2020-02-24 Andrew ReynoldsFixes for quantifiers documentation (#3811) tree | commitdiff
2020-02-24 Andrew ReynoldsUtilities for words (#3797) tree | commitdiff
2020-02-24 Andrew ReynoldsConvert parser input interface to api::Term (#3809) tree | commitdiff
2020-02-24 Abdalrhman MohamedFix bugs related to printing Sygus commands (#3804) tree | commitdiff
2020-02-24 Andrew ReynoldsAdd missing functions to new C++ API (#3769) tree | commitdiff
2020-02-24 Andres NoetzliMake lambda rewriter more robust (#3806) tree | commitdiff
2020-02-23 Andrew ReynoldsMinor refactoring of equality notifications (#3798) tree | commitdiff
2020-02-22 Andrew Reynolds Move check memberships to reg exp solver (#3793) tree | commitdiff
2020-02-22 Andrew ReynoldsMove cardinality inference scheme to base solver in... tree | commitdiff
2020-02-22 makaimannDump boolean propagations and conflicts for decision... tree | commitdiff
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741) tree | commitdiff
2020-02-21 Aina NiemetzNew C++ API: Remove TOTAL kinds. (#3794) tree | commitdiff
2020-02-21 Andrew ReynoldsSimple changes towards unicode string standard (#3791) tree | commitdiff
2020-02-21 Andrew V. JonesAdding checks to the validation of 'bv-sat-solver'... tree | commitdiff
2020-02-21 Andrew ReynoldsSplit extended functions solver in strings (#3768) tree | commitdiff
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) tree | commitdiff
2020-02-20 Andres NoetzliRemove unused code (#3782) tree | commitdiff
2020-02-20 Andrew ReynoldsMinor removals (#3786) tree | commitdiff
2020-02-20 Andres NoetzliRemove parser from bindings (#3779) tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2020-02-19 Andrew ReynoldsFix symmetry breaking for multiple sygus types (#3775) tree | commitdiff
2020-02-19 makaimannAdd Python bindings using Cython -- see below for more... tree | commitdiff
2020-02-19 Andrew ReynoldsDelay enumerative instantiation if theory engine does... tree | commitdiff
2020-02-19 Andrew ReynoldsChange Record to shared_ptr (#3778) tree | commitdiff
2020-02-19 Andrew ReynoldsFix approximate bounds for transcendental functions... tree | commitdiff
2020-02-19 makaimannChange datatype selector/constructor/tester to terms... tree | commitdiff
2020-02-18 Andrew ReynoldsAdd missing kinds for the new API (#3757) tree | commitdiff
2020-02-17 Andrew ReynoldsOption to limit the number of rounds of enumerative... tree | commitdiff
2020-02-17 Andrew Reynolds Fix soundness bug in reduction of integer div/mod... tree | commitdiff
2020-02-17 Haniel BarbosaUsing ParseOp in TPTP (#3764) tree | commitdiff
2020-02-17 Abdalrhman MohamedSupport dumping Sygus commands. (#3763) tree | commitdiff
2020-02-16 Andrew ReynoldsFix simple issue with cache (#3762) tree | commitdiff
2020-02-16 Andrew ReynoldsAdd temporary global API conversion utilities. (#3759) tree | commitdiff
2020-02-16 Andres NoetzliActivate reverse variant of F-Split inference (#3745) tree | commitdiff
2020-02-16 Andrew ReynoldsDisable regression (#3761) tree | commitdiff
2020-02-15 Andrew ReynoldsMove proxy variables to InferenceManager in strings... tree | commitdiff
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) tree | commitdiff
2020-02-14 Andrew ReynoldsUpdate sygus v1 parser to use ParseOp utility (#3756) tree | commitdiff
2020-02-14 Haniel BarbosaForcing rewrite pass rather than asserting if formula... tree | commitdiff
2020-02-13 Andrew ReynoldsConst input for sygus print callback (#3755) tree | commitdiff
2020-02-13 Andres Noetzli[Python] Properly destroy CVC4 object (#3753) tree | commitdiff
2020-02-12 Andres NoetzliRename Java package to edu.stanford.CVC4 (#3752) tree | commitdiff
2020-02-12 Andrew ReynoldsEnsure ext rewrites for associative ops dont throw... tree | commitdiff
2020-02-12 Andrew ReynoldsFix non-linear equality solving that involves mixed... tree | commitdiff
2020-02-11 Andrew ReynoldsFix term simplification based on entailment in quantifi... tree | commitdiff
2020-02-11 Andres NoetzliRemove `--strings-binary-csp` option (#3743) tree | commitdiff
2020-02-11 Andres NoetzliRefactor `CoreSolver::processSimpleNEq()` (#3736) tree | commitdiff
2020-02-11 Andrew ReynoldsUse example evaluation cache instead of sygus PBE ... tree | commitdiff
2020-02-11 Alex OzdemirImplement LFSCArithProof::equalityType. (#3740) tree | commitdiff
2020-02-10 Alex OzdemirAdd function for tightening literals (#3732) tree | commitdiff
2020-02-08 Andres NoetzliMake "unknown" non-critical for unsat cores check ... tree | commitdiff
2020-02-08 Andrew ReynoldsSplit strings finite model finding strategy (#3727) tree | commitdiff
2020-02-08 Andrew ReynoldsSplit core solver from the theory of strings (#3713) tree | commitdiff
2020-02-08 Andrew ReynoldsInterface for example evaluation cache utilities (... tree | commitdiff
next