--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of the justification SAT decision strategy
+ */
+
+#include "decision/justification_strategy.h"
+
+#include "prop/skolem_def_manager.h"
+
+using namespace cvc5::kind;
+using namespace cvc5::prop;
+
+namespace cvc5 {
+namespace decision {
+
+JustificationStrategy::JustificationStrategy(context::Context* c,
+ context::UserContext* u,
+ prop::SkolemDefManager* skdm)
+ : d_context(c),
+ d_cnfStream(nullptr),
+ d_satSolver(nullptr),
+ d_skdm(skdm),
+ d_assertions(
+ u,
+ c,
+ options::jhRlvOrder()), // assertions are user-context dependent
+ d_skolemAssertions(c, c), // skolem assertions are SAT-context dependent
+ d_justified(c),
+ d_stack(c),
+ d_lastDecisionLit(c),
+ d_currStatusDec(false),
+ d_useRlvOrder(options::jhRlvOrder()),
+ d_jhSkMode(options::jhSkolemMode()),
+ d_jhSkRlvMode(options::jhSkolemRlvMode())
+{
+}
+
+void JustificationStrategy::finishInit(CDCLTSatSolverInterface* ss,
+ CnfStream* cs)
+{
+ d_satSolver = ss;
+ d_cnfStream = cs;
+}
+
+void JustificationStrategy::presolve()
+{
+ d_lastDecisionLit = Node::null();
+ d_currUnderStatus = Node::null();
+ d_currStatusDec = false;
+ // reset the dynamic assertion list data
+ d_assertions.presolve();
+ d_skolemAssertions.presolve();
+ // clear the stack
+ d_stack.clear();
+}
+
+SatLiteral JustificationStrategy::getNext()
+{
+ // ensure we have an assertion
+ if (!refreshCurrentAssertion())
+ {
+ Trace("jh-process") << "getNext, already finished" << std::endl;
+ return undefSatLiteral;
+ }
+ Assert(d_stack.hasCurrentAssertion());
+ // temporary information in the loop below
+ JustifyInfo* ji;
+ JustifyNode next;
+ // we start with the value implied by the last decision, if it exists
+ SatValue lastChildVal = SAT_VALUE_UNKNOWN;
+ Trace("jh-process") << "getNext" << std::endl;
+ // If we had just sent a decision, then we lookup its value here. This may
+ // correspond to a context where the decision was carried out, or
+ // alternatively it may correspond to a case where we have backtracked and
+ // propagated that literal with opposite polarity. Thus, we do not assume we
+ // know the value of d_lastDecisionLit and look it up again here. The value
+ // of lastChildVal will be used to update the justify info in the current
+ // stack below.
+ if (!d_lastDecisionLit.get().isNull())
+ {
+ Trace("jh-process") << "last decision = " << d_lastDecisionLit.get()
+ << std::endl;
+ lastChildVal = lookupValue(d_lastDecisionLit.get());
+ if (lastChildVal == SAT_VALUE_UNKNOWN)
+ {
+ // if the value is now unknown, we must reprocess the assertion, since
+ // we have backtracked
+ TNode curr = d_stack.getCurrentAssertion();
+ d_stack.clear();
+ d_stack.reset(curr);
+ }
+ }
+ d_lastDecisionLit = TNode::null();
+ // while we are trying to satisfy assertions
+ do
+ {
+ Assert(d_stack.getCurrent() != nullptr);
+ // We get the next justify node, if it can be found.
+ do
+ {
+ // get the current justify info, which should be ready
+ ji = d_stack.getCurrent();
+ if (ji == nullptr)
+ {
+ break;
+ }
+ // get the next child to process from the current justification info
+ // based on the fact that its last child processed had value lastChildVal.
+ next = getNextJustifyNode(ji, lastChildVal);
+ // if the current node is finished, we pop the stack
+ if (next.first.isNull())
+ {
+ d_stack.popStack();
+ }
+ } while (next.first.isNull());
+
+ if (ji == nullptr)
+ {
+ // the assertion we just processed should have value true
+ Assert(lastChildVal == SAT_VALUE_TRUE);
+ if (!d_currUnderStatus.isNull())
+ {
+ // notify status if we are watching it
+ DecisionStatus ds;
+ if (d_currStatusDec)
+ {
+ ds = DecisionStatus::DECISION;
+ ++(d_stats.d_numStatusDecision);
+ }
+ else
+ {
+ ds = DecisionStatus::NO_DECISION;
+ ++(d_stats.d_numStatusNoDecision);
+ }
+ d_assertions.notifyStatus(d_currUnderStatus, ds);
+ }
+ // we did not find a next node for current, refresh current assertion
+ d_stack.clear();
+ refreshCurrentAssertion();
+ lastChildVal = SAT_VALUE_UNKNOWN;
+ Trace("jh-process") << "...exhausted assertion, now "
+ << d_stack.getCurrentAssertion() << std::endl;
+ }
+ else
+ {
+ // must have requested a next child to justify
+ Assert(!next.first.isNull());
+ Assert(next.second != SAT_VALUE_UNKNOWN);
+ // Look up whether the next child already has a value
+ lastChildVal = lookupValue(next.first);
+ if (lastChildVal == SAT_VALUE_UNKNOWN)
+ {
+ bool nextPol = next.first.getKind() != kind::NOT;
+ TNode nextAtom = nextPol ? next.first : next.first[0];
+ if (isTheoryAtom(nextAtom))
+ {
+ // should be assigned a literal
+ Assert(d_cnfStream->hasLiteral(nextAtom));
+ // get the SAT literal
+ SatLiteral nsl = d_cnfStream->getLiteral(nextAtom);
+ // flip if the atom was negated
+ // store the last decision value here, which will be used at the
+ // starting value on the next call to this method
+ lastChildVal = nextPol ? next.second : invertValue(next.second);
+ // (1) atom with unassigned value, return it as the decision, possibly
+ // inverted
+ Trace("jh-process")
+ << "...return " << nextAtom << " " << lastChildVal << std::endl;
+ // Note that the last child of the current node we looked at does
+ // *not* yet have a value. Although we are returning it as a decision,
+ // we cannot set its value in d_justified, because we have yet to
+ // push a decision level. Thus, we remember the literal we decided
+ // on. The value of d_lastDecisionLit will be processed at the
+ // beginning of the next call to getNext above.
+ d_lastDecisionLit = next.first;
+ // record that we made a decision
+ d_currStatusDec = true;
+ return lastChildVal == SAT_VALUE_FALSE ? ~nsl : nsl;
+ }
+ else
+ {
+ // NOTE: it may be the case that we have yet to justify this node,
+ // as indicated by the return of lookupValue. We may have a value
+ // assigned to next.first by the SAT solver, but we ignore it here.
+ // (2) unprocessed non-atom, push to the stack
+ d_stack.pushToStack(next.first, next.second);
+ d_stats.d_maxStackSize.maxAssign(d_stack.size());
+ // we have yet to process children for the next node, so lastChildVal
+ // remains set to SAT_VALUE_UNKNOWN.
+ }
+ }
+ else
+ {
+ Trace("jh-debug") << "in main loop, " << next.first << " has value "
+ << lastChildVal << std::endl;
+ }
+ // (3) otherwise, next already has a value lastChildVal which will be
+ // processed in the next iteration of the loop.
+ }
+ } while (d_stack.hasCurrentAssertion());
+ // we exhausted all assertions
+ Trace("jh-process") << "...exhausted all assertions" << std::endl;
+ return undefSatLiteral;
+}
+
+JustifyNode JustificationStrategy::getNextJustifyNode(
+ JustifyInfo* ji, prop::SatValue& lastChildVal)
+{
+ // get the node we are trying to justify and its desired value
+ JustifyNode jc = ji->getNode();
+ Assert(!jc.first.isNull());
+ Assert(jc.second != SAT_VALUE_UNKNOWN);
+ // extract the non-negated formula we are trying to justify
+ bool currPol = jc.first.getKind() != NOT;
+ TNode curr = currPol ? jc.first : jc.first[0];
+ Kind ck = curr.getKind();
+ // the current node should be a non-theory literal and not have double
+ // negation, due to our invariants of what is pushed onto the stack
+ Assert(!isTheoryAtom(curr));
+ Assert(ck != NOT);
+ // get the next child index to process
+ size_t i = ji->getNextChildIndex();
+ Trace("jh-debug") << "getNextJustifyNode " << curr << " / " << currPol
+ << ", index = " << i
+ << ", last child value = " << lastChildVal << std::endl;
+ // NOTE: if i>0, we just computed the value of the (i-1)^th child
+ // i.e. i == 0 || lastChildVal != SAT_VALUE_UNKNOWN,
+ // however this does not hold when backtracking has occurred.
+ // if i=0, we shouldn't have a last child value
+ Assert(i > 0 || lastChildVal == SAT_VALUE_UNKNOWN)
+ << "in getNextJustifyNode, value given for non-existent last child";
+ // we are trying to make the value of curr equal to currDesiredVal
+ SatValue currDesiredVal = currPol ? jc.second : invertValue(jc.second);
+ // value is set to TRUE/FALSE if the value of curr can be determined.
+ SatValue value = SAT_VALUE_UNKNOWN;
+ // if we require processing the next child of curr, we set desiredVal to
+ // value which we want that child to be to make curr's value equal to
+ // currDesiredVal.
+ SatValue desiredVal = SAT_VALUE_UNKNOWN;
+ if (ck == AND || ck == OR)
+ {
+ if (i == 0)
+ {
+ // See if a single child with currDesiredVal forces value, which is the
+ // case if ck / currDesiredVal in { and / false, or / true }.
+ if ((ck == AND) == (currDesiredVal == SAT_VALUE_FALSE))
+ {
+ // lookahead to determine if already satisfied
+ // we scan only once, when processing the first child
+ for (const Node& c : curr)
+ {
+ SatValue v = lookupValue(c);
+ if (v == currDesiredVal)
+ {
+ Trace("jh-debug") << "already forcing child " << c << std::endl;
+ value = currDesiredVal;
+ break;
+ }
+ // NOTE: if v == SAT_VALUE_UNKNOWN, then we can add this to a watch
+ // list and short circuit processing in the children of this node.
+ }
+ }
+ desiredVal = currDesiredVal;
+ }
+ else if ((ck == AND && lastChildVal == SAT_VALUE_FALSE)
+ || (ck == OR && lastChildVal == SAT_VALUE_TRUE)
+ || i == curr.getNumChildren())
+ {
+ Trace("jh-debug") << "current is forcing child" << std::endl;
+ // forcing or exhausted case
+ value = lastChildVal;
+ }
+ else
+ {
+ // otherwise, no forced value, value of child should match the parent
+ desiredVal = currDesiredVal;
+ }
+ }
+ else if (ck == IMPLIES)
+ {
+ if (i == 0)
+ {
+ // lookahead to second child to determine if value already forced
+ if (lookupValue(curr[1]) == SAT_VALUE_TRUE)
+ {
+ value = SAT_VALUE_TRUE;
+ }
+ else
+ {
+ // otherwise, we request the opposite of what parent wants
+ desiredVal = invertValue(currDesiredVal);
+ }
+ }
+ else if (i == 1)
+ {
+ // forcing case
+ if (lastChildVal == SAT_VALUE_FALSE)
+ {
+ value = SAT_VALUE_TRUE;
+ }
+ else
+ {
+ desiredVal = currDesiredVal;
+ }
+ }
+ else
+ {
+ // exhausted case
+ value = lastChildVal;
+ }
+ }
+ else if (ck == ITE)
+ {
+ if (i == 0)
+ {
+ // lookahead on branches
+ SatValue val1 = lookupValue(curr[1]);
+ SatValue val2 = lookupValue(curr[2]);
+ if (val1 == val2)
+ {
+ // branches have no difference, value is that of branches, which may
+ // be unknown
+ value = val1;
+ }
+ // if first branch is already wrong or second branch is already correct,
+ // try to make condition false. Note that we arbitrarily choose true here
+ // if both children are unknown. If both children have the same value
+ // and that value is not unknown, desiredVal will be ignored, since
+ // value is set above.
+ desiredVal =
+ (val1 == invertValue(currDesiredVal) || val2 == currDesiredVal)
+ ? SAT_VALUE_FALSE
+ : SAT_VALUE_TRUE;
+ }
+ else if (i == 1)
+ {
+ Assert(lastChildVal != SAT_VALUE_UNKNOWN);
+ // we just computed the value of the condition, check if the condition
+ // was false
+ if (lastChildVal == SAT_VALUE_FALSE)
+ {
+ // this increments to the else branch
+ i = ji->getNextChildIndex();
+ }
+ // make the branch equal to the desired value
+ desiredVal = currDesiredVal;
+ }
+ else
+ {
+ // return the branch value
+ value = lastChildVal;
+ }
+ }
+ else if (ck == XOR || ck == EQUAL)
+ {
+ Assert(curr[0].getType().isBoolean());
+ if (i == 0)
+ {
+ // check if the rhs forces a value
+ SatValue val1 = lookupValue(curr[1]);
+ if (val1 == SAT_VALUE_UNKNOWN)
+ {
+ // not forced, arbitrarily choose true
+ desiredVal = SAT_VALUE_TRUE;
+ }
+ else
+ {
+ // if the RHS of the XOR/EQUAL already had a value val1, then:
+ // ck / currDesiredVal
+ // equal / true ... LHS should have same value as RHS
+ // equal / false ... LHS should have opposite value as RHS
+ // xor / true ... LHS should have opposite value as RHS
+ // xor / false ... LHS should have same value as RHS
+ desiredVal = ((ck == EQUAL) == (currDesiredVal == SAT_VALUE_TRUE))
+ ? val1
+ : invertValue(val1);
+ }
+ }
+ else if (i == 1)
+ {
+ Assert(lastChildVal != SAT_VALUE_UNKNOWN);
+ // same as above, choosing a value for RHS based on the value of LHS,
+ // which is stored in lastChildVal.
+ desiredVal = ((ck == EQUAL) == (currDesiredVal == SAT_VALUE_TRUE))
+ ? lastChildVal
+ : invertValue(lastChildVal);
+ }
+ else
+ {
+ // recompute the value of the first child
+ SatValue val0 = lookupValue(curr[0]);
+ Assert(val0 != SAT_VALUE_UNKNOWN);
+ Assert(lastChildVal != SAT_VALUE_UNKNOWN);
+ // compute the value of the equal/xor. The values for LHS/RHS are
+ // stored in val0 and lastChildVal.
+ // (val0 == lastChildVal) / ck
+ // true / equal ... value of curr is true
+ // true / xor ... value of curr is false
+ // false / equal ... value of curr is false
+ // false / xor ... value of curr is true
+ value = ((val0 == lastChildVal) == (ck == EQUAL)) ? SAT_VALUE_TRUE
+ : SAT_VALUE_FALSE;
+ }
+ }
+ else
+ {
+ // curr should not be an atom
+ Assert(false);
+ }
+ // we return null if we have determined the value of the current node
+ if (value != SAT_VALUE_UNKNOWN)
+ {
+ Assert(!isTheoryAtom(curr));
+ // add to justify if so
+ d_justified.insert(curr, value);
+ // update the last child value, which will be used by the parent of the
+ // current node, if it exists.
+ lastChildVal = currPol ? value : invertValue(value);
+ Trace("jh-debug") << "getJustifyNode: return null with value "
+ << lastChildVal << std::endl;
+ // return null, indicating there is nothing left to do for current
+ return JustifyNode(TNode::null(), SAT_VALUE_UNKNOWN);
+ }
+ Trace("jh-debug") << "getJustifyNode: return " << curr[i]
+ << " with desired value " << desiredVal << std::endl;
+ // The next child should be a valid argument in curr. Otherwise, we did not
+ // recognize when its value could be inferred above.
+ Assert(i < curr.getNumChildren()) << curr.getKind() << " had no value";
+ // should set a desired value
+ Assert(desiredVal != SAT_VALUE_UNKNOWN)
+ << "Child " << i << " of " << curr.getKind() << " had no desired value";
+ // return the justify node
+ return JustifyNode(curr[i], desiredVal);
+}
+
+prop::SatValue JustificationStrategy::lookupValue(TNode n)
+{
+ bool pol = n.getKind() != NOT;
+ TNode atom = pol ? n : n[0];
+ Assert(atom.getKind() != NOT);
+ // check if we have already determined the value
+ // notice that d_justified may contain nodes that are not assigned SAT values,
+ // since this class infers when the value of nodes can be determined.
+ auto jit = d_justified.find(atom);
+ if (jit != d_justified.end())
+ {
+ return pol ? jit->second : invertValue(jit->second);
+ }
+ // Notice that looking up values for non-theory atoms may lead to
+ // an incomplete strategy where a formula is asserted but not justified
+ // via its theory literal subterms. This is the case because the justification
+ // heuristic is not the only source of decisions, as the theory may request
+ // them.
+ if (isTheoryAtom(atom))
+ {
+ SatLiteral nsl = d_cnfStream->getLiteral(atom);
+ prop::SatValue val = d_satSolver->value(nsl);
+ if (val != SAT_VALUE_UNKNOWN)
+ {
+ // this is the moment where we realize a skolem definition is relevant,
+ // add now.
+ // NOTE: if we enable skolems when they are justified, we could call
+ // a method notifyJustified(atom) here
+ d_justified.insert(atom, val);
+ return pol ? val : invertValue(val);
+ }
+ }
+ return SAT_VALUE_UNKNOWN;
+}
+
+bool JustificationStrategy::isDone() { return !refreshCurrentAssertion(); }
+
+void JustificationStrategy::addAssertion(TNode assertion)
+{
+ std::vector<TNode> toProcess;
+ toProcess.push_back(assertion);
+ insertToAssertionList(toProcess, false);
+}
+
+void JustificationStrategy::addSkolemDefinition(TNode lem, TNode skolem)
+{
+ if (d_jhSkRlvMode == options::JutificationSkolemRlvMode::ALWAYS)
+ {
+ // just add to main assertions list
+ std::vector<TNode> toProcess;
+ toProcess.push_back(lem);
+ insertToAssertionList(toProcess, false);
+ }
+}
+
+void JustificationStrategy::notifyAsserted(TNode n)
+{
+ if (d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT)
+ {
+ // assertion processed makes all skolems in assertion active,
+ // which triggers their definitions to becoming relevant
+ std::vector<TNode> defs;
+ d_skdm->notifyAsserted(n, defs, true);
+ insertToAssertionList(defs, true);
+ }
+ // NOTE: can update tracking triggers, pop stack to where a child implied
+ // that a node on the current stack is justified.
+}
+
+void JustificationStrategy::insertToAssertionList(std::vector<TNode>& toProcess,
+ bool useSkolemList)
+{
+ AssertionList& al = useSkolemList ? d_skolemAssertions : d_assertions;
+ IntStat& sizeStat =
+ useSkolemList ? d_stats.d_maxSkolemDefsSize : d_stats.d_maxAssertionsSize;
+ // always miniscope AND and negated OR immediately
+ size_t index = 0;
+ // must keep some intermediate nodes below around for ref counting
+ std::vector<Node> keep;
+ while (index < toProcess.size())
+ {
+ TNode curr = toProcess[index];
+ bool pol = curr.getKind() != NOT;
+ TNode currAtom = pol ? curr : curr[0];
+ index++;
+ Kind k = currAtom.getKind();
+ if (k == AND && pol)
+ {
+ toProcess.insert(toProcess.begin() + index, curr.begin(), curr.end());
+ }
+ else if (k == OR && !pol)
+ {
+ std::vector<Node> negc;
+ for (TNode c : currAtom)
+ {
+ Node cneg = c.negate();
+ negc.push_back(cneg);
+ // ensure ref counted
+ keep.push_back(cneg);
+ }
+ toProcess.insert(toProcess.begin() + index, negc.begin(), negc.end());
+ }
+ else if (!isTheoryAtom(currAtom))
+ {
+ al.addAssertion(curr);
+ // take stats
+ sizeStat.maxAssign(al.size());
+ }
+ else
+ {
+ // we skip (top-level) theory literals, since these are always propagated
+ // NOTE: skolem definitions that are always relevant should be added to
+ // assertions, for uniformity via a method notifyJustified(currAtom)
+ }
+ }
+ // clear since toProcess may contain nodes with 0 ref count after returning
+ // otherwise
+ toProcess.clear();
+}
+
+bool JustificationStrategy::refreshCurrentAssertion()
+{
+ // if we already have a current assertion, nothing to be done
+ TNode curr = d_stack.getCurrentAssertion();
+ if (!curr.isNull())
+ {
+ if (curr != d_currUnderStatus && !d_currUnderStatus.isNull())
+ {
+ ++(d_stats.d_numStatusBacktrack);
+ d_assertions.notifyStatus(d_currUnderStatus, DecisionStatus::BACKTRACK);
+ // we've backtracked to another assertion which may be partially
+ // processed. don't track its status?
+ d_currUnderStatus = Node::null();
+ // NOTE: could reset the stack here to preserve other invariants,
+ // currently we do not.
+ }
+ return true;
+ }
+ bool skFirst = (d_jhSkMode != options::JutificationSkolemMode::LAST);
+ // use main assertions first
+ if (refreshCurrentAssertionFromList(skFirst))
+ {
+ return true;
+ }
+ // if satisfied all main assertions, use the skolem assertions, which may
+ // fail
+ return refreshCurrentAssertionFromList(!skFirst);
+}
+
+bool JustificationStrategy::refreshCurrentAssertionFromList(bool useSkolemList)
+{
+ AssertionList& al = useSkolemList ? d_skolemAssertions : d_assertions;
+ bool doWatchStatus = !useSkolemList;
+ d_currUnderStatus = Node::null();
+ TNode curr = al.getNextAssertion();
+ SatValue currValue;
+ while (!curr.isNull())
+ {
+ // we never add theory literals to our assertions lists
+ Assert(!isTheoryLiteral(curr));
+ currValue = lookupValue(curr);
+ if (currValue == SAT_VALUE_UNKNOWN)
+ {
+ // if not already justified, we reset the stack and push to it
+ d_stack.reset(curr);
+ d_lastDecisionLit = TNode::null();
+ // for activity
+ if (doWatchStatus)
+ {
+ // initially, mark that we have not found a decision in this
+ d_currUnderStatus = d_stack.getCurrentAssertion();
+ d_currStatusDec = false;
+ }
+ return true;
+ }
+ // assertions should all be satisfied, otherwise we are in conflict
+ Assert(currValue == SAT_VALUE_TRUE);
+ if (doWatchStatus)
+ {
+ // mark that we did not find a decision in it
+ ++(d_stats.d_numStatusNoDecision);
+ d_assertions.notifyStatus(curr, DecisionStatus::NO_DECISION);
+ }
+ // already justified, immediately skip
+ curr = al.getNextAssertion();
+ }
+ return false;
+}
+
+bool JustificationStrategy::isTheoryLiteral(TNode n)
+{
+ return isTheoryAtom(n.getKind() == NOT ? n[0] : n);
+}
+
+bool JustificationStrategy::isTheoryAtom(TNode n)
+{
+ Kind k = n.getKind();
+ Assert(k != NOT);
+ return k != AND && k != OR && k != IMPLIES && k != ITE && k != XOR
+ && (k != EQUAL || !n[0].getType().isBoolean());
+}
+
+} // namespace decision
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of the justification SAT decision strategy
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__DECISION__JUSTIFICATION_STRATEGY_H
+#define CVC5__DECISION__JUSTIFICATION_STRATEGY_H
+
+#include "context/cdinsert_hashmap.h"
+#include "context/cdo.h"
+#include "decision/assertion_list.h"
+#include "decision/justify_info.h"
+#include "decision/justify_stack.h"
+#include "decision/justify_stats.h"
+#include "expr/node.h"
+#include "options/decision_options.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
+#include "prop/sat_solver_types.h"
+
+namespace cvc5 {
+
+namespace prop {
+class SkolemDefManager;
+}
+
+namespace decision {
+
+/**
+ * An implementation of justification SAT decision heuristic. This class
+ * is given access to the set of input formulas, and chooses next decisions
+ * based on the structure of the input formula.
+ *
+ * Notice that the SAT solver still propagates values for literals in the
+ * normal way based on BCP when using this SAT decision heuristic. This means
+ * that values for literals can be assigned between calls to get next
+ * decision. Thus, this module has access to the SAT solver for the purpose
+ * of looking up values already assigned to literals.
+ *
+ * One novel feature of this module is that it maintains a SAT-context-dependent
+ * stack corresponding to the current path in the input formula we are trying
+ * to satisfy. This means that computing the next decision does not require
+ * traversing the current assertion.
+ *
+ * As an example, say our input formulas are:
+ * (or (and A B) C D), (or E F)
+ * where A, B, C, D, E, F are theory literals. Moreover, say we are in a
+ * state where the SAT solver has initially assigned values:
+ * { A -> false, E -> true }
+ * Given a call to getNext, this module will analyze what is the next
+ * literal that would contribute towards making the input formulas evaluate to
+ * true. Assuming it works on assertions and terms left-to-right, it will
+ * perform the following reasoning:
+ * - The desired value of (or (and A B) C D) is true
+ * - The desired value of (and A B) is true
+ * - The desired value of A is true,
+ * ...The value of A was assigned false
+ * ...The value of (and A B) is false
+ * - Moving to the next literal, the desired value of C is true
+ * ...The value of C is unassigned, return C as a decision.
+ * After deciding C, assuming no backtracking occurs, we end up in a state
+ * where we have assigned:
+ * { A -> false, E -> true, C -> true }
+ * In the next call to getNext, this module will proceed, keeping the stack
+ * from the previous call:
+ * ... The value of C is true
+ * ... The value of (or (and A B) C D) is true
+ * - Moving to the next assertion, the desired value of (or E F) is true
+ * - The desired value of E is true
+ * ... The value of E is (already) assigned true
+ * ... the value of (or E F) is true.
+ * - The are no further assertions.
+ * Hence it will return the null SAT decision literal, indicating that no
+ * further decisions are necessary to satisfy the input assertions.
+ *
+ * This class has special handling of "skolem definitions", which arise when
+ * lemmas are introduced that correspond to the behavior of skolems. As an
+ * example, say our input, prior to preprocessing, is:
+ * (or (P (ite A 1 2)) Q)
+ * where P is an uninterpreted predicate of type Int -> Bool. After
+ * preprocessing, in particular term formula removal which replaces term-level
+ * ITE terms with fresh skolems, we get this set of assertions:
+ * (or (P k) Q), (ite A (= k 1) (= k 2))
+ * The second assertion is the skolem definition for k. Conceptually, this
+ * lemma is only relevant if we have asserted a literal that contains k.
+ * This module thus maintains two separate assertion lists, one for
+ * input assertions, and one for skolem definitions. The latter is populated
+ * only as skolems appear in assertions. In this example, we have initially:
+ * input assertions = { (or (P k) Q) }
+ * relevant skolem definitions = {}
+ * SAT context = {}
+ * Say this module returns (P k) as a decision. When this is asserted to
+ * the theory engine, a call to notifyAsserted is made with (P k). The
+ * skolem definition manager will recognize that (P k) contains k and hence
+ * its skolem definition is activated, giving us this state:
+ * input assertions = { (or (P k) Q) }
+ * relevant skolem definitions = { (ite A (= k 1) (= k 2)) }
+ * SAT context = { (P k) }
+ * We then proceed by satisfying (ite A (= k 1) (= k 2)), e.g. by returning
+ * A as a decision for getNext.
+ *
+ * Notice that the above policy allows us to ignore certain skolem definitions
+ * entirely. For example, if Q were to have been asserted instead of (P k),
+ * then (ite A (= k 1) (= k 2)) would not be added as a relevant skolem
+ * definition, and Q alone would have sufficed to show the input formula
+ * was satisfied.
+ */
+class JustificationStrategy
+{
+ public:
+ /** Constructor */
+ JustificationStrategy(context::Context* c,
+ context::UserContext* u,
+ prop::SkolemDefManager* skdm);
+
+ /** Finish initialize */
+ void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs);
+
+ /** Presolve, called at the beginning of each check-sat call */
+ void presolve();
+
+ /**
+ * Gets the next decision based on the current assertion to satisfy. This
+ * returns undefSatLiteral if there are no more assertions. In this case,
+ * all relevant input assertions are already propositionally satisfied by
+ * the current assignment.
+ *
+ * @return The next SAT literal to decide on.
+ */
+ prop::SatLiteral getNext();
+
+ /**
+ * Are we finished assigning values to literals?
+ *
+ * @return true if and only if all relevant input assertions are already
+ * propositionally satisfied by the current assignment.
+ */
+ bool isDone();
+
+ /**
+ * Notify this class that assertion is an (input) assertion, not corresponding
+ * to a skolem definition.
+ */
+ void addAssertion(TNode assertion);
+ /**
+ * Notify this class that lem is the skolem definition for skolem, which is
+ * a part of the current assertions.
+ */
+ void addSkolemDefinition(TNode lem, TNode skolem);
+ /**
+ * Notify this class that literal n has been asserted. This is triggered when
+ * n is sent to TheoryEngine. This activates skolem definitions for skolems
+ * k that occur in n.
+ */
+ void notifyAsserted(TNode n);
+
+ private:
+ /**
+ * Helper method to insert assertions in `toProcess` to `d_assertions` or
+ * `d_skolemAssertions` based on `useSkolemList`.
+ */
+ void insertToAssertionList(std::vector<TNode>& toProcess, bool useSkolemList);
+ /**
+ * Refresh current assertion. This ensures that d_stack has a current
+ * assertion to satisfy. If it does not already have one, we take the next
+ * assertion from the list of input assertions, or from the relevant
+ * skolem definitions based on the JutificationSkolemMode mode.
+ *
+ * @return true if we successfully initialized d_stack with the next
+ * assertion to satisfy.
+ */
+ bool refreshCurrentAssertion();
+ /**
+ * Implements the above function for the case where d_stack must get a new
+ * assertion to satisfy.
+ *
+ * @param useSkolemList If this is true, we pull the next assertion from
+ * the list of relevant skolem definitions.
+ * @return true if we successfully initialized d_stack with the next
+ * assertion to satisfy.
+ */
+ bool refreshCurrentAssertionFromList(bool useSkolemList);
+ /**
+ * Let n be the node referenced by ji.
+ *
+ * This method is called either when we have yet to process any children of n,
+ * or we just determined that the last child we processed of n had value
+ * lastChildVal.
+ *
+ * Note that knowing which child of n we processed last is the value of
+ * ji->d_childIndex.
+ *
+ * @param ji The justify node to process
+ * @param lastChildVal The value determined for the last child of the node of
+ * ji.
+ * @return Either (1) the justify node corresponding to the next child of n to
+ * consider adding to the stack, and its desired polarity, or
+ * (2) a null justify node and updates lastChildVal to the value of n.
+ */
+ JustifyNode getNextJustifyNode(JustifyInfo* ji, prop::SatValue& lastChildVal);
+ /**
+ * Returns the value TRUE/FALSE for n, or UNKNOWN otherwise.
+ *
+ * We return a value for n only if we have justified its values based on its
+ * children. For example, we return UNKNOWN for n of the form (and A B) if
+ * A and B have UNKNOWN value, even if the SAT solver has assigned a value for
+ * (internal) node n. If n itself is a theory literal, we lookup its value
+ * in the SAT solver if it is not already cached.
+ */
+ prop::SatValue lookupValue(TNode n);
+ /** Is n a theory literal? */
+ static bool isTheoryLiteral(TNode n);
+ /** Is n a theory atom? */
+ static bool isTheoryAtom(TNode n);
+ /** Pointer to the SAT context */
+ context::Context* d_context;
+ /** Pointer to the CNF stream */
+ prop::CnfStream* d_cnfStream;
+ /** Pointer to the SAT solver */
+ prop::CDCLTSatSolverInterface* d_satSolver;
+ /** Pointer to the skolem definition manager */
+ prop::SkolemDefManager* d_skdm;
+ /** The assertions, which are user-context dependent. */
+ AssertionList d_assertions;
+ /** The skolem assertions */
+ AssertionList d_skolemAssertions;
+
+ /** Mapping from non-negated nodes to their SAT value */
+ context::CDInsertHashMap<Node, prop::SatValue> d_justified;
+ /** A justify stack */
+ JustifyStack d_stack;
+ /** The last decision literal */
+ context::CDO<TNode> d_lastDecisionLit;
+ //------------------------------------ activity
+ /** Current assertion we are checking for status (context-independent) */
+ Node d_currUnderStatus;
+ /** Whether we have added a decision while considering d_currUnderStatus */
+ bool d_currStatusDec;
+ //------------------------------------ options
+ /** using relevancy order */
+ bool d_useRlvOrder;
+ /** skolem mode */
+ options::JutificationSkolemMode d_jhSkMode;
+ /** skolem relevancy mode */
+ options::JutificationSkolemRlvMode d_jhSkRlvMode;
+ /** The statistics */
+ JustifyStatistics d_stats;
+};
+
+} // namespace decision
+} // namespace cvc5
+
+#endif /* CVC5__DECISION__JUSTIFICATION_STRATEGY_H */
projects / cvc5.git / commitdiff