summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
AgeCommit message (Expand)Author
2018-10-23Sketch of refactoring the Commands to use new APInewApiForCommandsAndres Noetzli
2018-10-22Recover from wrong use of get-info :reason-unknown (#2667)Andres Noetzli
2018-10-19Sygus streaming non-implied predicates (#2660)Andrew Reynolds
2018-10-18Add OptionException handling during initialization (#2466)Andres Noetzli
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-10-17Sygus query generator (#2465)Andrew Reynolds
2018-10-15Delay initialization of theory engine (#2621)Andrew Reynolds
2018-10-12Reset input language for ExprMiner subsolver (#2624)Andres Noetzli
2018-10-10Fix default setting of CegisUnif options (#2605)Haniel Barbosa
2018-10-10Synthesize rewrite rules from inputs (#2608)Andrew Reynolds
2018-10-08Fix compiler warnings. (#2601)Aina Niemetz
2018-10-05Update default options for sygus (#2586)Andrew Reynolds
2018-10-01 Fix dumping pre/post preprocessing passes (#2469)Andres Noetzli
2018-10-01Refactor preprocessing pass registration (#2468)Andres Noetzli
2018-09-18Move and rename sygus solver classes (#2488)Andrew Reynolds
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-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-08Do beta-reduction in expandDefinitions (#2286)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback