include "pset05_definitions.dfy"

module Pset5 {
  import opened Defs

  // In this pset, you are asked to write (part of) the trivial algorithm for satisfiability (SAT) of Boolean formulas by enumerating all possible assignments, proving its correctness. Traditionally, the verification of a solver requires testing against millions of test cases with ground truth to avoid false negatives (which is also called incompleteness), and this process becomes hard as the Boolean formulas gets large. What you will do in this pset verifies correctness regardless of the size of the Boolean formulas. Sounds fun, right?
  // Please fill in "Your Spec" and "Your Code" throughout the file. You are free to create helper lemmas any way you'd like. You SHOULD NOT change any part of the given specifications or implementations otherwise.

  // We begin with an auxiliary function to enumerate all possible assignments for a Boolean formula, while passing the current assignment down.
  // Note that we help Dafny's termination checker by passing a *fuel* argument, which bounds how large a particular map is allowed to be.
  // You will need to add postconditions to the specifications of SATAux and SubstBF to get them to pass the checker. Please do NOT modify the function body of SATAux.
  function SATAux(fuel: nat, e: BooleanFormula, assignment: State): Option<State>
    requires |BFDomain(e)| == fuel
    // Your Spec
  {
    if fuel == 0 then
      if EvalBF(e, assignment) then Some(assignment) else None
    else
      match SATAux(fuel - 1, SubstBF(e, GetVariable(e), true), assignment[GetVariable(e) := true])
      case Some(a) => Some(a)
      case None => SATAux(fuel - 1, SubstBF(e, GetVariable(e), false), assignment[GetVariable(e) := false])
  }

  // Here we have the main algorithm that returns true if SATAux finds an assignment and false otherwise.
  predicate Satisfiable(e: BooleanFormula)
  {
    OptionToBool(SATAux(|BFDomain(e)|, e, map[]))
  }

  // Complete the main algorithm by writing the substitution function that replaces every occurrence of the "variable" with a constant "value" in a Boolean expression. You might also want to formulate and prove its specification for later use.
  function SubstBF(e: BooleanFormula, variable: string, value: bool): BooleanFormula
    // Your Spec
  {
    // Your Code
    Var("Placeholder")
  }

  // The correctness of our SAT solver is split into 2 parts. One is called the "soundness" of the solver, and it states that if it finds an assignment, then it is indeed a satisfying assignment. Prove that the auxiliary SAT function is sound.
  // Do NOT modify the specification of this lemma. If Dafny cannot prove the precondition of EvalBF here, consider adding a suitable postcondition to the specification of SATAux.
  lemma SATAuxSound(fuel: nat, e: BooleanFormula, assignment: State)
    requires |BFDomain(e)| == fuel
    ensures forall assignment' :: SATAux(fuel, e, assignment) == Some(assignment') ==> EvalBF(e, assignment') == true
  {
    // Your Code
  }

  // The second part of the correctness statement is called "completeness". It says if the solver finds no assignment to a formula, then none of the assignments satisfy the Boolean formula. Prove that the auxiliary SAT function is complete.
  lemma SATAuxComplete(fuel: nat, e: BooleanFormula, assignment: State)
    requires |BFDomain(e)| == fuel
    ensures SATAux(fuel, e, assignment) == None ==> forall a: State :: BFDomain(e) <= a.Keys ==> EvalBF(e, a) == false
  {
    // Your Code
  }

  // Our final theorem states that a Boolean formula is satisfiable if and only if there exists an assignment that evaluates to true. Use the previous 2 lemmas to prove this.
  lemma SATCorrect(e: BooleanFormula)
    ensures Satisfiable(e) <==> (exists assignment: State :: BFDomain(e) <= assignment.Keys && EvalBF(e, assignment) == true)
  {
    // Your Code
  }

  // There is another formulation for the correctness of our SAT solver. Namely, the set of all satisfiable assignments of a Boolean formula is nonempty if and only if it is satisfiable. Formally state this theorem and prove it's correct by completing the following function.

  // The first function generates a set of all possible assignments for the input variables.
  function AllAssignments(s: set<string>): set<State>
  {
    if s == {}
    then
      // The base case is a set with trivial assignment
      {map[]}
    else
      // Fill in the inductive case. Recall the example of SetHasMinimum in class 9 and implement a similar method below to help you finish the inductive case. Also remember set/map comprehensions can come in handy.
      // Your Code
      {map["Placeholder" := false]}
  }

  // Implement SetHasMinimum just like in class 9.
  lemma SetHasMinimum(s: set<string>)
    requires s != {}
    ensures exists n: string :: n in s && forall m: string :: m in s ==> StrLe(n, m)
  {
    // The following line asserts that the string comparison (StrLe) implements a total order and is required for Dafny to figure out the uniqueness of the minimum. For the case of set<nat>, this fact is already known by Dafny.
    // If you run into timeout problems, it's because Dafny constantly tries to rewrite using the 4 ensures of StrLeTotallyOrdered. Try to spell out more hints to Dafny so that it gets to the right conclusion faster. Or even better, insert StrLeRefl, StrLeTrans, StrLeAntisym, StrLeTotal just at the right places to have Dafny solve it in less than a second.
    StrLeTotallyOrdered();
    // Your Code
  }

  // This is the SetMinimum function like in class 9.
  function SetMinimum(s: set<string>): string
    requires s != {}
    ensures SetMinimum(s) in s
  {
    // The following line is again required
    StrLeTotallyOrdered();
    // Your Code
    "Placeholder"
  }

  // Prove the following lemma to make sure you got the right implementation for AllAssignments, and to use later.
  lemma AllAssignmentsCorrect(s: set<string>)
    ensures forall a: State :: (a.Keys == s) <==> a in AllAssignments(s)
  {
    // Your Code
  }

  // Now we restrict the set so that it only contains the assignments that satisfy e. We provide its specification to make sure your implementation is correct.
  function SatisfiableAssignments(e: BooleanFormula): set<State>
    ensures forall a: State :: (a.Keys == BFDomain(e) && EvalBF(e, a)) <==> a in SatisfiableAssignments(e)
  {
    // Your Code
    {map["Placeholder" := false]}
  }

  // Last, we are here at our final lemma that states that e is satisfiable if and only if its SatisfiableAssignments is not empty. Recall the proof techniques from class 10. You may find it easier to directly reason about it using SATCorrect, instead of proving by induction all over again.
  lemma SATCorrect2(e: BooleanFormula)
    ensures Satisfiable(e) <==> (SatisfiableAssignments(e) != {})
  {
    // Your Code
  }

}