projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-08-31 Andrew ReynoldsBasic proof support in inference manager (#4975) commit | commitdiff | tree
2020-08-29 Andrew Reynolds(proof-new) More term context utilities. (#4912) commit | commitdiff | tree
2020-08-29 Mathias PreinerNew C++ API: Add REGEXP_{REPEAT,LOOP}_OP handling in... commit | commitdiff | tree
2020-08-28 Andrew ReynoldsReplace Theory::Set with TheoryIdSet (#4959) commit | commitdiff | tree
2020-08-28 yoni206Incremental support for bv_to_int (#4967) commit | commitdiff | tree
2020-08-28 Andrew Reynolds(proof-new) Make CombinationEngine proof producing... commit | commitdiff | tree
2020-08-28 Andrew Reynolds(new theory) Update TheoryQuantifiers to the new interf... commit | commitdiff | tree
2020-08-28 Andrew Reynolds(proof-new) Add the SMT proof post processor (#4913) commit | commitdiff | tree
2020-08-28 Andrew Reynolds(new theory) Update TheoryFP to the new interface ... commit | commitdiff | tree
2020-08-28 Gereon Kremer(cad-solver) Fixed excluding lemma generation. (#4958) commit | commitdiff | tree
2020-08-28 Andrew ReynoldsDo not delay processing equivalence class merges in... commit | commitdiff | tree
2020-08-28 Andrew ReynoldsAdd the buffered inference manager (#4954) commit | commitdiff | tree
2020-08-28 Andrew Reynolds(new theory) Update TheorySep to new interface (#4947) commit | commitdiff | tree
2020-08-28 Gereon KremerMake iand lemmas use proper Inference types. (#4956) commit | commitdiff | tree
2020-08-27 Andrew Reynolds(proof-new) Add the proof equality engine (#4881) commit | commitdiff | tree
2020-08-27 Andrew ReynoldsAdd irrelevant kinds infrastructure to TheoryModel... commit | commitdiff | tree
2020-08-27 Andrew ReynoldsAdd the theory inference manager (#4948) commit | commitdiff | tree
2020-08-27 Andrew Reynolds(new theory) Update TheoryUF to new interface (#4944) commit | commitdiff | tree
2020-08-26 Andrew ReynoldsConnect combination engine to theory engine (#4940) commit | commitdiff | tree
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... commit | commitdiff | tree
2020-08-25 Haniel BarbosaEliminating spurious replay of commands for define... commit | commitdiff | tree
2020-08-25 Andrew ReynoldsAdd the combination engine (#4939) commit | commitdiff | tree
2020-08-24 Andrew ReynoldsAdd a few basic extensions for equality engine (#4937) commit | commitdiff | tree
2020-08-24 Gereon KremerFix memory issue in AntlrInput::parseError (#4873) commit | commitdiff | tree
2020-08-24 Andrew ReynoldsDo not use relevance during non-linear check model... commit | commitdiff | tree
2020-08-24 Mathias PreinerIncrease regress level to 2 for production build. ... commit | commitdiff | tree
2020-08-24 Andrew ReynoldsAdd the distributed model manager (#4934) commit | commitdiff | tree
2020-08-24 Andrew ReynoldsExtend the standard Theory template based on equality... commit | commitdiff | tree
2020-08-22 Andrew ReynoldsRemove unecessary theory model builder base class ... commit | commitdiff | tree
2020-08-21 Andrew ReynoldsDynamic allocation of model equality engine (#4911) commit | commitdiff | tree
2020-08-21 Andrew ReynoldsLimit trigger terms to shared terms in arrays (#4932) commit | commitdiff | tree
2020-08-21 Andrew ReynoldsRemove spurious theory methods calls (#4931) commit | commitdiff | tree
2020-08-21 Andrew ReynoldsConnect the relevance manager to TheoryEngine and use... commit | commitdiff | tree
2020-08-21 Andrew ReynoldsSimplify and fix care graph for ufHo (#4924) commit | commitdiff | tree
2020-08-21 Andrew ReynoldsRemove BV equality slicer (#4928) commit | commitdiff | tree
2020-08-20 Andrew ReynoldsAdd TheoryState objects to each Theory (#4920) commit | commitdiff | tree
2020-08-20 Andrew ReynoldsSplit QuantElimSolver from SmtEngine (#4919) commit | commitdiff | tree
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ... commit | commitdiff | tree
2020-08-20 Andrew ReynoldsRemove example theory (#4922) commit | commitdiff | tree
2020-08-20 Andrew ReynoldsAdd strings-exp to regression (#4923) commit | commitdiff | tree
2020-08-19 Gereon Kremer(cad solver) Add a partial check method. (#4904) commit | commitdiff | tree
2020-08-19 Andrew ReynoldsMake sets and strings solver states inherit from Theory... commit | commitdiff | tree
2020-08-19 Andres NoetzliRequire `--strings-exp` when using `str.substr` (#4916) commit | commitdiff | tree
2020-08-19 Gereon KremerChanges assertion (about maximum set cardinality) to... commit | commitdiff | tree
2020-08-19 Andres Noetzli[Regressions] Do not test `--check-proofs` anymore... commit | commitdiff | tree
2020-08-19 Gereon KremerFix SmtEngine::reset() (#4917) commit | commitdiff | tree
2020-08-18 Abdalrhman... Refactor functions that print commands (Part 2) (#4905) commit | commitdiff | tree
2020-08-18 Andrew Reynolds(proof-new) Theory preprocessor proof producing (#4807) commit | commitdiff | tree
2020-08-18 Andrew ReynoldsIntroduce the theory state object (#4910) commit | commitdiff | tree
2020-08-18 Andrew ReynoldsStandardize collectModelInfo and theory-specific collec... commit | commitdiff | tree
2020-08-18 Andrew Reynolds(proof-new) Minor updates to trust node (#4900) commit | commitdiff | tree
2020-08-18 Andrew Reynolds(proof-new) SMT proof postprocess callback (#4883) commit | commitdiff | tree
2020-08-18 Andrew ReynoldsQuantifiers engine stores a pointer to the master equal... commit | commitdiff | tree
2020-08-18 Andrew ReynoldsSplit SygusSolver from SmtEngine (#4891) commit | commitdiff | tree
2020-08-18 Andrew ReynoldsAdd the relevance manager module (#4894) commit | commitdiff | tree
2020-08-18 Andrew Reynolds(proof-new) Callbacks for term-context-sensitive terms... commit | commitdiff | tree
2020-08-17 Alex OzdemirAdd identifier name for side condition. (#4902) commit | commitdiff | tree
2020-08-17 Andres Noetzli[CI] Update package list (#4906) commit | commitdiff | tree
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) commit | commitdiff | tree
2020-08-17 Andrew Reynolds(proof-new) Prepare the theory of strings for proof... commit | commitdiff | tree
2020-08-16 Andrew ReynoldsAdd non-emptiness to conclusion of positive RE star... commit | commitdiff | tree
2020-08-16 Gereon Kremer(cad solver) Use the current model as initial assignmen... commit | commitdiff | tree
2020-08-15 Andrew ReynoldsMinor cleanup related to notifications (#4898) commit | commitdiff | tree
2020-08-15 Andrew ReynoldsAdd finishInit method to PropEngine (#4895) commit | commitdiff | tree
2020-08-15 Andrew Reynolds(proof-new) Add the strings proof checker (#4858) commit | commitdiff | tree
2020-08-14 Andrew ReynoldsSimplify equality engine notifications (#4896) commit | commitdiff | tree
2020-08-14 E Polgreencorrectly parse sygus lang option (#4884) commit | commitdiff | tree
2020-08-14 Gereon KremerInspect roots to avoid certain resultants (Algorithm... commit | commitdiff | tree
2020-08-13 Andrew ReynoldsSplit SmtSolver from SmtEngine (#4880) commit | commitdiff | tree
2020-08-13 Andrew ReynoldsFixes for corner case of decision tree learning with... commit | commitdiff | tree
2020-08-13 Andrew ReynoldsMore basic fix for dumping synth-fun (#4886) commit | commitdiff | tree
2020-08-13 Andrew ReynoldsAdd the distributed equality engine manager (#4867) commit | commitdiff | tree
2020-08-13 Haniel Barbosa[proof-new] Adding support for corner case of transitiv... commit | commitdiff | tree
2020-08-12 Haniel Barbosageneralize handling MERGED_THROUGH_CONSTANST in EqProof... commit | commitdiff | tree
2020-08-12 Abdalrhman... Refactor functions that print commands (Part 1) (#4869) commit | commitdiff | tree
2020-08-12 Andrew ReynoldsFixes for degenerate case of sygus decision tree learni... commit | commitdiff | tree
2020-08-12 Andrew Reynolds(proof-new) Improve robustness of CONG rule (#4882) commit | commitdiff | tree
2020-08-12 Andrew Reynolds(proof-new) Proof support in the strings term registry... commit | commitdiff | tree
2020-08-12 Andrew Reynolds(proof-new) Improve interfaces to proof generators... commit | commitdiff | tree
2020-08-12 makaimannAdd option to only build library (#4801) commit | commitdiff | tree
2020-08-12 Andrew Reynolds(proof-new) Witness form proof generator (#4782) commit | commitdiff | tree
2020-08-12 Gereon KremerAdd naive support for integer variables. (#4835) commit | commitdiff | tree
2020-08-12 Haniel Barbosa(proof-new) Improving proof-production in Equality... commit | commitdiff | tree
2020-08-12 Andrew ReynoldsFix connection to master equality engine in sets (... commit | commitdiff | tree
2020-08-12 Gereon KremerFix infinite loop in arith_ite_simp (#4805) commit | commitdiff | tree
2020-08-12 Andrew ReynoldsFix unsupported option in regress1. (#4874) commit | commitdiff | tree
2020-08-12 Andrew ReynoldsSplit SmtEngineState from SmtEngine (#4855) commit | commitdiff | tree
2020-08-12 Andrew ReynoldsPrepare theory of sets for dynamic allocation of equali... commit | commitdiff | tree
2020-08-12 Andrew ReynoldsFinal preparations for changing API to use the Node... commit | commitdiff | tree
2020-08-12 Andrew Reynolds(proof-new) Extensions to proof checker interface ... commit | commitdiff | tree
2020-08-11 Andrew ReynoldsUpdate Expr-level unit tests that depend on datatypes... commit | commitdiff | tree
2020-08-11 Andrew ReynoldsRemove instantiation model true option (#4861) commit | commitdiff | tree
2020-08-11 Aina NiemetzNew C++ API: Remove redundant API functions for mkReal... commit | commitdiff | tree
2020-08-09 Andrew ReynoldsMake valuation class more robust to null underlying... commit | commitdiff | tree
2020-08-09 Andrew ReynoldsSplitting a few utility classes from EqualityEngine... commit | commitdiff | tree
2020-08-08 Andrew ReynoldsMove datatype index constant to its own file (#4859) commit | commitdiff | tree
2020-08-07 Aina NiemetzGH Actions: Remove cancel action. (#4843) commit | commitdiff | tree
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr... commit | commitdiff | tree
2020-08-06 Andrew ReynoldsSplit preprocessor from SmtEngine (#4854) commit | commitdiff | tree
2020-08-06 Andrew Reynolds(proof-new) Refactor regular expression operation ... commit | commitdiff | tree
next