projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Allow to pass ProofGenerator to arithmetic inference manager. (#5488)
[cvc5.git] / src /
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference... tree | commitdiff
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... tree | commitdiff
2020-11-19 Aina Niemetzfloatingpoint.h: Split in preparation to cleanly separa... tree | commitdiff
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472) tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422) tree | commitdiff
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic... tree | commitdiff
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-11-18 Mathias PreinerAdd -> operator overload for cd* iterators. (#5464) tree | commitdiff
2020-11-18 Andrew ReynoldsAdd let binding utility (#5444) tree | commitdiff
2020-11-18 Andrew ReynoldsMinor cleanup of SmtEngine (#5450) tree | commitdiff
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... tree | commitdiff
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) tree | commitdiff
2020-11-18 Andrew ReynoldsFix asan issues related to solver and symbol manager... tree | commitdiff
2020-11-18 Aina NiemetzFloatingPoint: Use uint32_t instead of unsigned. (... tree | commitdiff
2020-11-18 Aina NiemetzFloatingPoint: Clean up and document header, format... tree | commitdiff
2020-11-17 Gereon KremerFix tangent plane lemmas (#5455) tree | commitdiff
2020-11-16 Gereon KremerRefactor tangent plane lemmas (#5449) tree | commitdiff
2020-11-16 Andrew ReynoldsCleaning up scopes in preparation for symbol manager... tree | commitdiff
2020-11-16 Gereon KremerImprove accuracy of resource limitation (#4763) tree | commitdiff
2020-11-14 Andrew ReynoldsFix double conflict in extended string solver (#5435) tree | commitdiff
2020-11-14 Andrew Reynolds(proof-new) Proofs for non-clausal simplification ... tree | commitdiff
2020-11-13 Andrew Reynolds(proof-new) Enable proofs for datatypes (#5436) tree | commitdiff
2020-11-13 yoni206Model declarations printing options (#5432) tree | commitdiff
2020-11-13 Andrew ReynoldsAdd more features to symbol manager (#5434) tree | commitdiff
2020-11-13 Andrew ReynoldsMake regular expression difference left associative... tree | commitdiff
2020-11-12 Andrew ReynoldsSimplify sygus solver and sygus stream (#5389) tree | commitdiff
2020-11-12 Andrew ReynoldsFix printing of define named function (#5425) tree | commitdiff
2020-11-12 yoni206Models standard (#5415) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Separate explanation stages in proof equali... tree | commitdiff
2020-11-12 Andrew ReynoldsFix redundant refinement lemma in sygus solver (#5399) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Proofs for skolemization (#5339) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Fix true explanations of propagations in... tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Improve printing and debugging for pedantic... tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Add datatypes inference to proof constructo... tree | commitdiff
2020-11-12 Andrew ReynoldsMake symbol manager context dependent (#5424) tree | commitdiff
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) tree | commitdiff
2020-11-11 Andrew ReynoldsRewrite witness terms at prerewrite (#5419) tree | commitdiff
2020-11-11 Andrew ReynoldsAdd simple substitution utility (#5397) tree | commitdiff
2020-11-11 Andrew ReynoldsPass symbol manager to commands (#5410) tree | commitdiff
2020-11-11 Andrew ReynoldsFix preregistration in TheorySep before declare-heap... tree | commitdiff
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... tree | commitdiff
2020-11-10 Andrew ReynoldsMake mkGroundTerm deterministic (#5347) tree | commitdiff
2020-11-10 Andrew ReynoldsAdd getSubtermKinds to node algorithm (#5398) tree | commitdiff
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... tree | commitdiff
2020-11-10 Andrew ReynoldsMigrate some documentation about attributes (#5390) tree | commitdiff
2020-11-09 Andrew ReynoldsAdd symbol manager (#5380) tree | commitdiff
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) tree | commitdiff
2020-11-09 Gereon KremerProperly clear interrupt for solve() as well. (#5403) tree | commitdiff
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) tree | commitdiff
2020-11-06 mudathirmahgoubFix issue #5342 (#5349) tree | commitdiff
2020-11-06 Andrew Reynolds(proof-new) Miscellaneous changes to strings for proofs... tree | commitdiff
2020-11-06 Andrew ReynoldsSplit sygus template inference to its own file (#5388) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366) tree | commitdiff
2020-11-04 Andres NoetzliAdd constants from equality engine evaluation to model... tree | commitdiff
2020-11-03 Andrew ReynoldsAdd scope methods constructing types in API (#5393) tree | commitdiff
2020-11-03 Andres NoetzliAdd support for printing `re.loop` and `re.^` (#5392) tree | commitdiff
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386) tree | commitdiff
2020-11-03 Andrew ReynoldsMove sygus qe preproc to its own file (#5375) tree | commitdiff
2020-11-02 Andrew ReynoldsUpdate strings proxy variable map to be context indepen... tree | commitdiff
2020-11-02 Andrew ReynoldsMiscellaneous cleaning of parser (#5369) tree | commitdiff
2020-11-02 Andrew ReynoldsAvoid dynamic allocation in symbol table implementation... tree | commitdiff
2020-10-30 Gereon KremerUse BoundInference in nonlinear extension (#5359) tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-29 Andrew ReynoldsSet strings pending conflict flag (#5364) tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
2020-10-29 Andrew Reynolds(proof-new) Update the strings inference manager for... tree | commitdiff
2020-10-29 Gereon KremerAdd NodeManager::mkOr() (#5360) tree | commitdiff
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) tree | commitdiff
2020-10-28 Andrew ReynoldsFixes for unconstrained variables in nonlinear model... tree | commitdiff
2020-10-28 Andrew ReynoldsConvert symbol table from Expr-level to Term-level... tree | commitdiff
2020-10-28 Gereon KremerSplit NlSolver in multiple subsolvers (#5315) tree | commitdiff
2020-10-28 Andrew ReynoldsAdd rewrites for div/mod in the arithmetic rewriter... tree | commitdiff
2020-10-27 Abdalrhman MohamedRefactor DeclareSygusVarCommand and SynthFunCommand... tree | commitdiff
2020-10-27 Andrew ReynoldsAdd missing methods involving datatype sorts to the... tree | commitdiff
2020-10-27 Gereon KremerDisable --nl-cad option by default (#5350) tree | commitdiff
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345) tree | commitdiff
2020-10-27 mudathirmahgoubAdd DUPICATE_REMOVAL operator to bags (#5336) tree | commitdiff
2020-10-26 Andrew Reynolds(proof-new) Add datatypes proof checker (#5340) tree | commitdiff
2020-10-26 Andrew ReynoldsSend external equalities from collapse selector as... tree | commitdiff
2020-10-24 mudathirmahgoubFix issue 5271 (#5335) tree | commitdiff
2020-10-24 Haniel Barbosa[proof-new] Fix n-ary kind handling in EqEngine explana... tree | commitdiff
2020-10-23 Andrew ReynoldsApply alpha equivalence to annotated quantified formula... tree | commitdiff
2020-10-23 Andrew ReynoldsChange datatypes lemma policy for equalities not coming... tree | commitdiff
2020-10-23 Andrew ReynoldsFix related to preregistering boolean term variables... tree | commitdiff
2020-10-22 Gereon KremerUse theoryof-mode=type for QF_NRA (#5326) tree | commitdiff
2020-10-22 Andrew ReynoldsRemove unused equality engine types (#5319) tree | commitdiff
2020-10-22 mudathirmahgoubFix issue 5309 (#5327) tree | commitdiff
2020-10-22 Andrew Reynolds(proof-new) Make theory preprocessor user-context depen... tree | commitdiff
2020-10-21 Gereon Kremer(proof-new) Make circuit propagator proof producing... tree | commitdiff
2020-10-21 mudathirmahgoubImplement bags evaluator (#5322) tree | commitdiff
2020-10-21 Alex Ozdemir(proof-new) Add arith proof macros file to CMake (... tree | commitdiff
2020-10-21 Alex Ozdemir(proof-new) arith: dedup literals in flattenImpl (... tree | commitdiff
2020-10-21 Andrew Reynolds(proof-new) Updates to lazy proof chain (#5317) tree | commitdiff
2020-10-21 mudathirmahgoubAdd operator MakeBagOp for constructing bags (#5209) tree | commitdiff
2020-10-21 Abdalrhman MohamedAdd finishInit for getInterpol and getAbduct. (#5316) tree | commitdiff
2020-10-21 Andrew Reynolds(proof-new) Fixes for proofs in rewriter (#5307) tree | commitdiff
2020-10-20 Aina NiemetzFix compiler warnings. (#5305) tree | commitdiff
2020-10-20 Gereon Kremer(proof-new) Add proofs for circuit propagator (#5301) tree | commitdiff
next