projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Integer: CLN: Move implementation of member functions to .cpp file. (#5304)
2020-10-11 Gereon KremerAdd conversion of poly polynomial to cvc node. (#5218)
 commit | commitdiff | tree
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic...
commit | commitdiff | tree
2020-10-02 Gereon KremerAllow for theory combination of strings with nonlinear...
commit | commitdiff | tree
2020-10-01 Gereon KremerAllow to use the initial assignment for CAD (#5177)
 commit | commitdiff | tree
2020-09-30 Gereon KremerRemove too strict assertion to allow for approximate...
commit | commitdiff | tree
2020-09-30 Gereon KremerAdd missing includes. (#5170)
 commit | commitdiff | tree
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160)
 commit | commitdiff | tree
2020-09-29 Gereon KremerClean up nonlinear extension (#5149)
 commit | commitdiff | tree
2020-09-28 Gereon KremerAdd new arithmetic BoundInference class (#5148)
 commit | commitdiff | tree
2020-09-26 Gereon KremerUse inference manager for nl_solver (#5125)
 commit | commitdiff | tree
2020-09-23 Gereon KremerMake IAND solver use inference manager. (#5126)
 commit | commitdiff | tree
2020-09-22 Gereon KremerICP-based solver for nonlinear arithmetic (#5017)
 commit | commitdiff | tree
2020-09-17 Gereon Kremer(cad-solver) Fix square-free-basis computation (#5085)
 commit | commitdiff | tree
2020-09-17 Gereon KremerUse new inference manager in transcendental solver...
commit | commitdiff | tree
2020-09-04 Gereon KremerUse arith::InferenceManager for CAD lemmas (#5015)
 commit | commitdiff | tree
2020-09-03 Gereon KremerAdded a new rule to simplify (bvugt (bvurem T x) x...
commit | commitdiff | tree
2020-09-03 Gereon KremerBasic integration of arith::InferenceManager (#4999)
 commit | commitdiff | tree
2020-09-03 Gereon KremerMake nonlinear extension (more) deterministic (#4996)
 commit | commitdiff | tree
2020-09-02 Gereon KremerRemove #line directives from generated files. (#5005)
 commit | commitdiff | tree
2020-09-02 Gereon KremerUse std::unique_ptr instead of std::shared_ptr for...
commit | commitdiff | tree
2020-09-02 Gereon KremerAdd ArithLemma and arith::InferenceManager (#4960)
 commit | commitdiff | tree
2020-08-31 Gereon KremerFix --ackermann in the presence on syntactically different...
commit | commitdiff | tree
2020-08-28 Gereon Kremer(cad-solver) Fixed excluding lemma generation. (#4958)
 commit | commitdiff | tree
2020-08-28 Gereon KremerMake iand lemmas use proper Inference types. (#4956)
 commit | commitdiff | tree
2020-08-24 Gereon KremerFix memory issue in AntlrInput::parseError (#4873)
 commit | commitdiff | tree
2020-08-19 Gereon Kremer(cad solver) Add a partial check method. (#4904)
 commit | commitdiff | tree
2020-08-19 Gereon KremerChanges assertion (about maximum set cardinality) to...
commit | commitdiff | tree
2020-08-19 Gereon KremerFix SmtEngine::reset() (#4917)
 commit | commitdiff | tree
2020-08-16 Gereon Kremer(cad solver) Use the current model as initial assignment...
commit | commitdiff | tree
2020-08-14 Gereon KremerInspect roots to avoid certain resultants (Algorithm...
commit | commitdiff | tree
2020-08-12 Gereon KremerAdd naive support for integer variables. (#4835)
 commit | commitdiff | tree
2020-08-12 Gereon KremerFix infinite loop in arith_ite_simp (#4805)
 commit | commitdiff | tree
2020-08-05 Gereon KremerImprove error message for unsupported exponents (#4852)
 commit | commitdiff | tree
2020-08-05 Gereon KremerAdd dummy returns if libpoly is unavailable. (#4845)
 commit | commitdiff | tree
2020-08-04 Gereon KremerProperly initialize d_fullyInited. (#4840)
 commit | commitdiff | tree
2020-08-04 Gereon KremerAdd CAD-based solver (#4834)
 commit | commitdiff | tree
2020-07-30 Gereon KremerCad implementation (#4774)
 commit | commitdiff | tree
2020-07-30 Gereon KremerAdds the interface for the CAD-based arithmetic solver...
commit | commitdiff | tree
2020-07-21 Gereon KremerPreparations for a CAD-based arithmetic solver (#4762)
 commit | commitdiff | tree
2020-07-17 Gereon KremerIntegration of libpoly (#4679)
 commit | commitdiff | tree
2020-07-16 Gereon KremerResource manager cleanup (#4732)
 commit | commitdiff | tree
2020-07-16 Gereon KremerRemove cumulative time limits and cpu time limits ...
commit | commitdiff | tree
2020-07-16 Gereon KremerFixes memory leak when an exception goes through runCvc4...
commit | commitdiff | tree
2020-07-15 Gereon KremerAdd missing header (Fixes #4743) (#4749)
 commit | commitdiff | tree
2020-07-13 Gereon KremerImplement --tlimit for windows (#4716)
 commit | commitdiff | tree
2020-07-10 Gereon KremerAdd deps/install/lib to RPATH and warn user when using...
commit | commitdiff | tree
2020-07-08 Gereon KremerRe-implement handling of --tlimit (#4655)
 commit | commitdiff | tree