projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)
2021-01-25 mudathirmahgoubrename InferInfo::d_newSkolem to InferInfo::d_skolems...
commit | commitdiff | tree
2021-01-24 Andrew Reynolds Initial cleaning of e-matching instantiation strategy...
commit | commitdiff | tree
2021-01-24 Andrew ReynoldsInitial cleaning of triggers (#5795)
 commit | commitdiff | tree
2021-01-24 Andrew ReynoldsInitial cleaning of inst match generator (#5794)
 commit | commitdiff | tree
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768)
 commit | commitdiff | tree
2021-01-24 Andrew ReynoldsAdd interface for getting preprocessed term (#5798)
 commit | commitdiff | tree
2021-01-22 Haniel Barbosa[proof-new] Expanding MACRO_RESOLUTION in post-processing...
commit | commitdiff | tree
2021-01-21 Andrew ReynoldsAdd div, mod, abs in non-strict parsing mode (#5793)
 commit | commitdiff | tree
2021-01-21 Alex Ozdemirarith: Proofs for Diophantine cuts (#5792)
 commit | commitdiff | tree
2021-01-20 Andrew ReynoldsRefactoring the single invocation solver (#5706)
 commit | commitdiff | tree
2021-01-20 Andrew ReynoldsFix type issues with relevant domain computation (...
commit | commitdiff | tree
2021-01-20 Andrew ReynoldsFix corner case of wrongly applied selector as trigger...
commit | commitdiff | tree
2021-01-20 Andrew ReynoldsDo not track processed in remove term formulas loop...
commit | commitdiff | tree
2021-01-20 Aina NiemetzSMT2 parser: Do not add non-linear symbols for linear...
commit | commitdiff | tree
2021-01-20 Andrew ReynoldsUse arbitrary ground term assignment for sorts where...
commit | commitdiff | tree
2021-01-19 Alex OzdemirImplement proofs for arith BRAB lemmas (#5784)
 commit | commitdiff | tree
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass...
commit | commitdiff | tree
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776)
 commit | commitdiff | tree
2021-01-13 Andrew ReynoldsSplit eager solver from strings solver state (#5775)
 commit | commitdiff | tree
2021-01-13 Ying ShengAdd unit test for api getInterpolant() -- issue #5593...
commit | commitdiff | tree
2021-01-13 Andrew ReynoldsDo not call ppRewrite on Boolean equalities (#5762)
 commit | commitdiff | tree
2021-01-12 Aina Niemetzgoogle test: expr: Migrate node_black. (#5764)
 commit | commitdiff | tree
2021-01-12 Aina Niemetzgoogle test: Use ASSERT_* instead of EXPECT_*. (#5765)
 commit | commitdiff | tree
2021-01-12 yoni206Foreign theory rewrite option (#5763)
 commit | commitdiff | tree
2021-01-11 Andrew ReynoldsMerge theory registrar and theory proxy (#5758)
 commit | commitdiff | tree
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing...
commit | commitdiff | tree
2021-01-11 Andrew ReynoldsRemove extended rewrite for arithmetic (#5760)
 commit | commitdiff | tree
2021-01-09 yoni206Strings arith checks preprocessing pass: step 2 (#5750)
 commit | commitdiff | tree
2021-01-09 mudathirmahgoubFix issue 5513 (#5757)
 commit | commitdiff | tree
2021-01-08 mudathirmahgoubRename getAntecedent to getPremises (#5754)
 commit | commitdiff | tree
2021-01-08 Haniel Barbosa[proof-new] Implementing getProof in the API and SMT...
commit | commitdiff | tree
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731)
 commit | commitdiff | tree
2021-01-08 yoni206bv-to-int: avoid binarizing nodes twice (#5749)
 commit | commitdiff | tree
2021-01-07 Gereon KremerMake sure polynomials are properly factorized in nl...
commit | commitdiff | tree
2021-01-07 Haniel BarbosaRemove dependency on expression layer in TPTP parser...
commit | commitdiff | tree
2021-01-07 Haniel BarbosaFix warning in TPTP parser (#5752)
 commit | commitdiff | tree
2021-01-06 yoni206strings arith checks preprocessing pass: step 1 (#5747)
 commit | commitdiff | tree
2021-01-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory...
commit | commitdiff | tree
2021-01-05 yoni206Adding str.len to triggers (#5746)
 commit | commitdiff | tree
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer...
commit | commitdiff | tree
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if...
commit | commitdiff | tree
2020-12-23 Haniel BarbosaDumping unsat cores after check-sat-assuming/QUERY...
commit | commitdiff | tree
2020-12-23 Andrew ReynoldsAdd option to track and notify from CNF stream (#5708)
 commit | commitdiff | tree
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716)
 commit | commitdiff | tree
2020-12-23 Haniel Barbosa[proof-new] Adding a manager for the new unsat cores...
commit | commitdiff | tree
2020-12-23 Andrew Reynolds(proof-new) Miscelleneous fixes from proof-new (#5714)
 commit | commitdiff | tree
2020-12-23 Gereon KremerAdd proofs for nonlinear sign lemmas. (#5707)
 commit | commitdiff | tree
2020-12-23 Andrew ReynoldsMinor simplification to Theory::theoryOf (#5719)
 commit | commitdiff | tree
2020-12-22 yoni206Delete duplicated code (#5718)
 commit | commitdiff | tree
2020-12-22 Andrew ReynoldsMove slow regression to regress3 (#5715)
 commit | commitdiff | tree
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessing...
commit | commitdiff | tree
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713)
 commit | commitdiff | tree
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709)
 commit | commitdiff | tree
2020-12-21 Haniel BarbosaHave unsat core regression agnostic to number of assertions...
commit | commitdiff | tree
2020-12-21 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy...
commit | commitdiff | tree
2020-12-21 Gereon KremerAdd proof for sine shift lemmas. (#5710)
 commit | commitdiff | tree
2020-12-21 Gereon Kremer(proof-new) Make nl-ext factoring lemmas proof producing...
commit | commitdiff | tree
2020-12-21 Andrew ReynoldsEliminate recursion from the internals of term formula...
commit | commitdiff | tree
2020-12-21 Andrew ReynoldsFix issue with selector triggers (#5689)
 commit | commitdiff | tree
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendental...
commit | commitdiff | tree
2020-12-18 Andrew ReynoldsSimplify internal API for sygus (#5687)
 commit | commitdiff | tree
2020-12-18 Gereon KremerAdd proof checker for nl tangent lemma (#5704)
 commit | commitdiff | tree
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ...
commit | commitdiff | tree
2020-12-18 Gereon Kremer(proof-new) Add proof for tangent plane lemmas (#5700)
 commit | commitdiff | tree
2020-12-18 Gereon KremerAdd proof for split zero check. (#5699)
 commit | commitdiff | tree
2020-12-17 Andrew Reynolds(proof-new) Minor updates to term conversion proof...
commit | commitdiff | tree
2020-12-17 Gereon KremerAlways consider rewritten lemmas for caching. (#5696)
 commit | commitdiff | tree
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext...
commit | commitdiff | tree
2020-12-17 Andrew ReynoldsSimplify term formula removal interface (#5695)
 commit | commitdiff | tree
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685)
 commit | commitdiff | tree
2020-12-17 Haniel Barbosa[proof-new] Only use old proof code for unsat cores...
commit | commitdiff | tree
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647)
 commit | commitdiff | tree
2020-12-16 Andrew ReynoldsMark quantifier instantiations as needs justify (#5684)
 commit | commitdiff | tree
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682)
 commit | commitdiff | tree
2020-12-16 mudathirmahgoubRenamed InferInfo::getAntecedant to InferInfo::getAntecedent...
commit | commitdiff | tree
2020-12-16 Andrew Reynolds(proof-new) Use bound variable manager (#5679)
 commit | commitdiff | tree
2020-12-16 Andrew ReynoldsMove ownership of term formula removal to theory preprocesso...
commit | commitdiff | tree
2020-12-16 Andrew ReynoldsUse uint64 utility when parsing tuple selectors in...
commit | commitdiff | tree
2020-12-15 Andrew ReynoldsMove trigger trie to own file (#5680)
 commit | commitdiff | tree
2020-12-15 Andrew ReynoldsImprovements related to quantifiers printing (#5678)
 commit | commitdiff | tree
2020-12-15 Andrew ReynoldsProper expand definitions for sets (#5676)
 commit | commitdiff | tree
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conjecture...
commit | commitdiff | tree
2020-12-15 Andrew ReynoldsFix datatypes compute ground value (#5671)
 commit | commitdiff | tree
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672)
 commit | commitdiff | tree
2020-12-15 Gereon KremerAdd getters to retrieve constants from api::Term (...
commit | commitdiff | tree
2020-12-14 Haniel Barbosa[proof-new] Making the CDCL(T) Minisat proof producing...
commit | commitdiff | tree
2020-12-14 Haniel Barbosa[proof-new] Make prop engine proof producing (#5667)
 commit | commitdiff | tree
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624)
 commit | commitdiff | tree
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine...
commit | commitdiff | tree
2020-12-14 Andrew Reynolds(proof-new) Add bound variable manager (#5655)
 commit | commitdiff | tree
2020-12-14 Andrew ReynoldsFix and improve evaluator (#5563)
 commit | commitdiff | tree
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistration...
commit | commitdiff | tree
2020-12-12 Andrew ReynoldsFlush statistics through NodeManager in SmtEngine ...
commit | commitdiff | tree
2020-12-11 yoni206bv-to-int: new tests from an issue (#5654)
 commit | commitdiff | tree
2020-12-11 Haniel Barbosa [proof-new] Updating theory proxy to new proof infrastructu...
commit | commitdiff | tree
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623)
 commit | commitdiff | tree
2020-12-10 Gereon KremerRefactor KindMap (#5646)
 commit | commitdiff | tree
2020-12-10 Aina Niemetzgoogle test: expr: Migrate node_algorithm_black. (...
commit | commitdiff | tree
2020-12-10 Andrew ReynoldsRefactor regressions (#5639)
 commit | commitdiff | tree
2020-12-10 Aina Niemetzgoogle test: expr: Migrate kind_black. (#5634)
 commit | commitdiff | tree
next