projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Simplify method for inferring proxy lemmas in strings (#5789)
2021-02-10 Andrew ReynoldsSimplify method for inferring proxy lemmas in strings...
commit | commitdiff | tree
2021-02-10 Andrew ReynoldsRemove track instantiations infrastructure (#5883)
 commit | commitdiff | tree
2021-02-10 Andrew ReynoldsOptimize get skolems method (#5876)
 commit | commitdiff | tree
2021-02-10 Andrew ReynoldsDo not traverse quantifiers in term formula removal...
commit | commitdiff | tree
2021-02-09 Andrew ReynoldsEliminating dependencies from inst utils (#5882)
 commit | commitdiff | tree
2021-02-09 Andrew ReynoldsMake term database optionally SAT-context-dependent...
commit | commitdiff | tree
2021-02-08 Andrew ReynoldsUse quantifiers inference manager for lemma management...
commit | commitdiff | tree
2021-02-08 Andrew ReynoldsFix disequality between seq.unit terms (#5880)
 commit | commitdiff | tree
2021-02-08 Andrew ReynoldsRemove support for inst closure (#5874)
 commit | commitdiff | tree
2021-02-08 Andrew ReynoldsAvoid spurious traversal of terms during preregistration...
commit | commitdiff | tree
2021-02-06 Andrew ReynoldsDo not combine theories if theory engine needs check...
commit | commitdiff | tree
2021-02-05 Andrew ReynoldsMinor cleaning of quantifiers engine (#5858)
 commit | commitdiff | tree
2021-02-05 Andrew ReynoldsMiscellaneous cleaning in theory engine (#5854)
 commit | commitdiff | tree
2021-02-04 Andrew ReynoldsIntroduce quantifiers registry utility (#5829)
 commit | commitdiff | tree
2021-02-04 Andrew ReynoldsEliminate equality query dependence on quantifiers...
commit | commitdiff | tree
2021-02-02 Andrew Reynolds(proof-new) Miscellaneous fixes and regressions (#5841)
 commit | commitdiff | tree
2021-02-02 Andrew Reynolds(proof-new) Refactor theory preprocessing (#5835)
 commit | commitdiff | tree
2021-02-02 Andrew ReynoldsRemove quantifiers regression from decision folder...
commit | commitdiff | tree
2021-02-02 Andrew ReynoldsCleanup some includes (#5847)
 commit | commitdiff | tree
2021-02-02 Andrew ReynoldsImprovements for NL traces (#5846)
 commit | commitdiff | tree
2021-02-01 Andrew ReynoldsEliminate PREPROCESS lemma property (#5827)
 commit | commitdiff | tree
2021-02-01 Andrew ReynoldsSimplify alpha equivalence module (#5839)
 commit | commitdiff | tree
2021-01-30 Andrew ReynoldsFix unguarded call to get representative (#5838)
 commit | commitdiff | tree
2021-01-29 Andrew Reynolds(proof-new) Distinguish pre vs post rewrites in term...
commit | commitdiff | tree
2021-01-28 Andrew ReynoldsReorganize calls to quantifiers engine from SmtEngine...
commit | commitdiff | tree
2021-01-28 Andrew ReynoldsSimplify lemma interface (#5819)
 commit | commitdiff | tree
2021-01-28 Andrew ReynoldsUse standard equality engine information in quantifiers...
commit | commitdiff | tree
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817)
 commit | commitdiff | tree
2021-01-27 Andrew ReynoldsAdd option for whether to filter candidate rewrite...
commit | commitdiff | tree
2021-01-27 Andrew ReynoldsSplit pattern term selector from trigger (#5811)
 commit | commitdiff | tree
2021-01-27 Andrew Reynolds(proof-new) Improvements to quantifiers engine and...
commit | commitdiff | tree
2021-01-27 Andrew ReynoldsUse term canonizer utility locally in quantifiers ...
commit | commitdiff | tree
2021-01-27 Andrew ReynoldsUse standard conflict mechanism in quantifiers state...
commit | commitdiff | tree
2021-01-26 Andrew ReynoldsIntroduce quantifiers inference manager (#5821)
 commit | commitdiff | tree
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820)
 commit | commitdiff | tree
2021-01-26 Andrew ReynoldsRefactor quantifiers engine initialization (#5813)
 commit | commitdiff | tree
2021-01-25 Andrew ReynoldsEnsure uses of ground terms in triggers are preprocessed...
commit | commitdiff | tree
2021-01-25 Andrew ReynoldsSplit inst match generator into multiple files (#5805)
 commit | commitdiff | tree
2021-01-25 Andrew ReynoldsSplit E-matching strategies to own files (#5807)
 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-21 Andrew ReynoldsAdd div, mod, abs in non-strict parsing mode (#5793)
 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 Andrew ReynoldsUse arbitrary ground term assignment for sorts where...
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 Andrew ReynoldsDo not call ppRewrite on Boolean equalities (#5762)
 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-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory...
commit | commitdiff | tree
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer...
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 Andrew Reynolds(proof-new) Miscelleneous fixes from proof-new (#5714)
 commit | commitdiff | tree
2020-12-23 Andrew ReynoldsMinor simplification to Theory::theoryOf (#5719)
 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 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy...
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 Andrew ReynoldsSimplify internal API for sygus (#5687)
 commit | commitdiff | tree
2020-12-17 Andrew Reynolds(proof-new) Minor updates to term conversion proof...
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-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 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-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624)
 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 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623)
 commit | commitdiff | tree
2020-12-10 Andrew ReynoldsRefactor regressions (#5639)
 commit | commitdiff | tree
2020-12-09 Andrew Reynolds(proof-new) Make theory preprocessor proofs self contained...
commit | commitdiff | tree
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline...
commit | commitdiff | tree
2020-12-09 Andrew ReynoldsRemove obsolete regressions (#5633)
 commit | commitdiff | tree
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when...
commit | commitdiff | tree
2020-12-09 Andrew ReynoldsDo not check FP at last call if not necessary (#5627)
 commit | commitdiff | tree
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware...
commit | commitdiff | tree
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequences...
commit | commitdiff | tree
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences...
commit | commitdiff | tree
next