summaryrefslogtreecommitdiff
path: root/src/prop
AgeCommit message (Expand)Author
2021-11-12Remove `ConstantMap<Rational>` (#7635)Andres Noetzli
2021-11-06Remove `Notice()` in favor of new `verbose()` (#7588)Gereon Kremer
2021-11-05[proofs] Fix open sat proof (#7509)Haniel Barbosa
2021-11-04Replace the old dump infrastructure (#7572)Andrew Reynolds
2021-11-01bv: Remove layered solver. (#7455)Mathias Preiner
2021-10-26[proofs] Reset local var in SatProofManager since incremental exists (#7500)Haniel Barbosa
2021-10-21[proofs] Fix open proof in SAT solver due to cycles (#7448)Haniel Barbosa
2021-10-11Rename SmtScope to SolverEngineScope. (#7284)Aina Niemetz
2021-10-08Make skolem definition manager robust to function skolems (#7327)Andrew Reynolds
2021-10-08Add argument to distinguish lemmas and input assertions (#7326)Andrew Reynolds
2021-10-07Use skolem lemma in prop layer interfaces (#7320)Andrew Reynolds
2021-10-07Eliminate more circular dependencies on solver engine (#7311)Andrew Reynolds
2021-10-06Refactor skolem definitions notifications for the decision engine (#7310)Andrew Reynolds
2021-10-04Make decision engine use env (#7300)Andrew Reynolds
2021-10-01Update theory preprocessor to use Env (#7288)Andrew Reynolds
2021-09-30Rename SmtEngine to SolverEngine. (#7282)Aina Niemetz
2021-09-14Add get-difficulty to the API (#7194)Andrew Reynolds
2021-09-02Implement lazy proof checking modes (#7106)Andrew Reynolds
2021-09-01[proof] [sat] Fix lost reference to reason when processing redundant literals...Haniel Barbosa
2021-08-19[unsat cores] [proofs] Revert test about when to explain propagations (#7034)Haniel Barbosa
2021-08-18Make TheoryProxy use Env, simplify initialization of PropEngine (#7031)Andrew Reynolds
2021-08-03Remove dependencies on smt engine in smt solver (#6965)Andrew Reynolds
2021-07-14[proof] Fix open proof issues in SAT proof (#6887)Haniel Barbosa
2021-07-13[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)Haniel Barbosa
2021-07-09Implement stop-only for new justification heuristic (#6847)Andrew Reynolds
2021-06-30Use SAT context level for --bv-assert-input instead of decision level. (#6758)Mathias Preiner
2021-06-21Move cnfConversionTime statistic to CnfStream. (#6769)Mathias Preiner
2021-06-21Make CaDiCaL a required dependency. (#6761)Mathias Preiner
2021-06-18Make CnfStream::toCNF iterative (#6757)Mathias Preiner
2021-06-15Remove public option wrappers (#6716)Gereon Kremer
2021-06-07Remove `Options::wasSetByUser()` (#6682)Gereon Kremer
2021-05-27Update proof namespaces (#6614)Andrew Reynolds
2021-05-27Enable new justification heuristic by default (#6613)Andrew Reynolds
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
2021-05-20Properly initialize. (#6586)Gereon Kremer
2021-05-20Remove old unsat cores (#6581)Haniel Barbosa
2021-05-19Correctly handle negated assertions for assumption-based unsat cores. (#6579)Mathias Preiner
2021-05-17Include cinttypes instead of inttypes.h (#6548)Andres Noetzli
2021-05-14bv: Assert input facts on user-level 0. (#6515)Mathias Preiner
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-04Move current decision engine to decision engine old (#6466)Andrew Reynolds
2021-05-04Move env into smt solver, theory engine, prop engine (#6486)Andrew Reynolds
2021-05-04Do not use proof CNF stream with assumptions-based cores (#6488)Haniel Barbosa
2021-04-28Make sure reference stats are reset properly (#6457)Gereon Kremer
2021-04-26First part of options refactoring (#6428)Gereon Kremer
2021-04-26Fix assertions in SAT solver (#6443)Haniel Barbosa
2021-04-23Add assumption-based unsat cores. (#6427)Mathias Preiner
2021-04-23Make sure a ReferenceStat is set to values of the correct type (#6430)Gereon Kremer
2021-04-22 Reorganizing use of skolem definition manager in prop engine (#6415)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback