summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2018-09-22cmake: Remove unused CMakeLists.txtMathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-18Move and rename sygus solver classes (#2488)Andrew Reynolds
2018-09-18fix assertion error (#2487)Haniel Barbosa
2018-09-17Remove broken dumping support from portfolio build (#2470)Andres Noetzli
2018-09-17Remove unnecessary tracing from preprocessing (#2472)Andres Noetzli
2018-09-14Refactor how assertions are added to decision engine (#2396)Andres Noetzli
2018-09-11Support model cores via option --produce-model-cores. (#2407)Andrew Reynolds
2018-09-10Refactor non-clausal simplify preprocessing pass. (#2425)Aina Niemetz
2018-09-05Finer-grained inference of substitutions in incremental mode (#2403)Andrew Reynolds
2018-09-04Transfer ownership of learned literals from SMT engine to circuit propagator....Aina Niemetz
2018-09-04Fix merge mishap of #2359.Aina Niemetz
2018-08-30Refactor theory preprocess into preprocessing pass. (#2395)Mathias Preiner
2018-08-29Refactor MipLibTrick preprocessing pass. (#2359)Mathias Preiner
2018-08-28Move flag needsFinish from SMT engine to circuit propagator.Aina Niemetz
2018-08-25Refactor unconstrained simplification pass (#2374)Andres Noetzli
2018-08-25Refactor quantifier macros preprocessing pass (#1840)yoni206
2018-08-24Refactor nlExtPurify preprocessing pass (#1963)Haniel Barbosa
2018-08-24 Remove spurious disabling of cbqi-all (#2368)Andrew Reynolds
2018-08-23 Do not print internally generated datatypes in external outputs with sygus (...Andrew Reynolds
2018-08-23Makes the filename be set in the SMT engine by default (#2366)Haniel Barbosa
2018-08-23Refactor ITE simplification preprocessing pass. (#2360)Aina Niemetz
2018-08-23Use "filename" instead of "name" in SmtEngine::setInfo() (#2361)Andres Noetzli
2018-08-22global-negate preprocessing pass (#2317)yoni206
2018-08-21Removing unused bool members in command.cpp. Also initializes a bool member. ...Tim King
2018-08-21Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350)Mathias Preiner
2018-08-21Use cbqi-full for sygus (#2346)Andrew Reynolds
2018-08-20 Make sygus inference a preprocessing pass (#2334)Andrew Reynolds
2018-08-17 Eliminate partial operators in sygus grammar normalization (#2323)Andrew Reynolds
2018-08-16Refactor eager atoms preprocessing pass. (#2318)Mathias Preiner
2018-08-17cleaning unnecessary timers/dumps (#2327)Haniel Barbosa
2018-08-16Make quantifiers-preprocess preprocessing pass (#2322)Caleb Donovick
2018-08-16Refactor IteRemoval preprocessing pass (#1793)Andres Noetzli
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-08-16Refactor extended rewriter preprocessing pass (#2324)Haniel Barbosa
2018-08-16Refactor apply2const (#2316)Haniel Barbosa
2018-08-15Remove unused tuple classes (#2313)Andres Noetzli
2018-08-15Make sort inference a preprocessing pass (#2309)Andrew Reynolds
2018-08-15Fix dumping of get-unsat-assumptions (#2302)Andres Noetzli
2018-08-13Fix get-unsat-assumptions output (#2301)Andres Noetzli
2018-08-08Do beta-reduction in expandDefinitions (#2286)Andrew Reynolds
2018-08-07Require Swig 3 (#2283)Andres Noetzli
2018-08-07Delete functions instead of using CVC4_UNDEFINED (#1794)Andres Noetzli
2018-08-06 Move sygus quantifier elimination step for non-ground-single-invocation to s...Andrew Reynolds
2018-08-06Fixes for sygus inference (#2238)Andrew Reynolds
2018-08-01Remove outdated references to TLS (#2245)Andres Noetzli
2018-08-01Fix issues with printing parametric datatypes in smt2 (#2213)Andrew Reynolds
2018-07-31Improvements and tests for the API around separation logic (#2229)ayveejay
2018-07-31Fix option handler for lazy/bv-sat-solver combinations. (#2225)Mathias Preiner
2018-07-30Add support for incremental eager bit-blasting. (#1838)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback