diff options
Diffstat (limited to 'src')
168 files changed, 1430 insertions, 487 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5362baad8..0bdd1c4fe 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -29,6 +29,8 @@ libcvc5_add_sources( decision/decision_strategy.h decision/justification_heuristic.cpp decision/justification_heuristic.h + decision/justification_strategy.cpp + decision/justification_strategy.h decision/justify_info.cpp decision/justify_info.h decision/justify_stack.cpp @@ -136,9 +138,50 @@ libcvc5_add_sources( printer/smt2/smt2_printer.h printer/tptp/tptp_printer.cpp printer/tptp/tptp_printer.h + proof/buffered_proof_generator.cpp + proof/buffered_proof_generator.h + proof/conv_proof_generator.cpp + proof/conv_proof_generator.h + proof/conv_seq_proof_generator.cpp + proof/conv_seq_proof_generator.h proof/clause_id.h proof/dot/dot_printer.cpp proof/dot/dot_printer.h + proof/eager_proof_generator.cpp + proof/eager_proof_generator.h + proof/lazy_proof.cpp + proof/lazy_proof.h + proof/lazy_proof_chain.cpp + proof/lazy_proof_chain.h + proof/lazy_tree_proof_generator.cpp + proof/lazy_tree_proof_generator.h + proof/proof.cpp + proof/proof.h + proof/proof_checker.cpp + proof/proof_checker.h + proof/proof_ensure_closed.cpp + proof/proof_ensure_closed.h + proof/proof_generator.cpp + proof/proof_generator.h + proof/proof_node.cpp + proof/proof_node.h + proof/proof_node_algorithm.cpp + proof/proof_node_algorithm.h + proof/proof_node_to_sexpr.cpp + proof/proof_node_to_sexpr.h + proof/proof_node_manager.cpp + proof/proof_node_manager.h + proof/proof_node_updater.cpp + proof/proof_node_updater.h + proof/proof_rule.cpp + proof/proof_rule.h + proof/proof_set.h + proof/proof_step_buffer.cpp + proof/proof_step_buffer.h + proof/trust_node.cpp + proof/trust_node.h + proof/theory_proof_step_buffer.cpp + proof/theory_proof_step_buffer.h proof/unsat_core.cpp proof/unsat_core.h prop/bv_sat_solver_notify.h @@ -600,8 +643,6 @@ libcvc5_add_sources( theory/decision_manager.h theory/decision_strategy.cpp theory/decision_strategy.h - theory/eager_proof_generator.cpp - theory/eager_proof_generator.h theory/ee_manager.cpp theory/ee_manager.h theory/ee_manager_distributed.cpp @@ -631,8 +672,6 @@ libcvc5_add_sources( theory/inference_id.h theory/inference_manager_buffered.cpp theory/inference_manager_buffered.h - theory/lazy_tree_proof_generator.cpp - theory/lazy_tree_proof_generator.h theory/logic_info.cpp theory/logic_info.h theory/model_manager.cpp @@ -1029,14 +1068,10 @@ libcvc5_add_sources( theory/theory_model_builder.h theory/theory_preprocessor.cpp theory/theory_preprocessor.h - theory/theory_proof_step_buffer.cpp - theory/theory_proof_step_buffer.h theory/theory_rewriter.cpp theory/theory_rewriter.h theory/theory_state.cpp theory/theory_state.h - theory/trust_node.cpp - theory/trust_node.h theory/trust_substitutions.cpp theory/trust_substitutions.h theory/type_enumerator.h diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index d56f594ce..53ea46f46 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -112,5 +112,3 @@ add_jar(cvc5jar ) add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5) - -get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE)
\ No newline at end of file diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp new file mode 100644 index 000000000..80fca23d5 --- /dev/null +++ b/src/decision/justification_strategy.cpp @@ -0,0 +1,649 @@ +/****************************************************************************** + * 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 diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h new file mode 100644 index 000000000..2fa216487 --- /dev/null +++ b/src/decision/justification_strategy.h @@ -0,0 +1,265 @@ +/****************************************************************************** + * 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 */ diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 9bf63dcfc..094c7bcbd 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -24,8 +24,6 @@ libcvc5_add_sources( attribute_unique_id.h bound_var_manager.cpp bound_var_manager.h - buffered_proof_generator.cpp - buffered_proof_generator.h emptyset.cpp emptyset.h emptybag.cpp @@ -33,10 +31,6 @@ libcvc5_add_sources( expr_iomanip.cpp expr_iomanip.h kind_map.h - lazy_proof.cpp - lazy_proof.h - lazy_proof_chain.cpp - lazy_proof_chain.h match_trie.cpp match_trie.h node.cpp @@ -58,37 +52,12 @@ libcvc5_add_sources( sequence.cpp sequence.h node_visitor.h - proof.cpp - proof.h - proof_checker.cpp - proof_checker.h - proof_ensure_closed.cpp - proof_ensure_closed.h - proof_generator.cpp - proof_generator.h - proof_node.cpp - proof_node.h - proof_node_algorithm.cpp - proof_node_algorithm.h - proof_node_to_sexpr.cpp - proof_node_to_sexpr.h - proof_node_manager.cpp - proof_node_manager.h - proof_node_updater.cpp - proof_node_updater.h - proof_rule.cpp - proof_rule.h - proof_set.h - proof_step_buffer.cpp - proof_step_buffer.h skolem_manager.cpp skolem_manager.h symbol_manager.cpp symbol_manager.h symbol_table.cpp symbol_table.h - tconv_seq_proof_generator.cpp - tconv_seq_proof_generator.h term_canonize.cpp term_canonize.h term_context.cpp @@ -97,8 +66,6 @@ libcvc5_add_sources( term_context_node.h term_context_stack.cpp term_context_stack.h - term_conversion_proof_generator.cpp - term_conversion_proof_generator.h type_checker.h type_matcher.cpp type_matcher.h diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 4004bf6fe..8e1c5e54c 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -53,6 +53,7 @@ const char* toString(SkolemFunId id) case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG"; case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR"; case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB"; + case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT"; default: return "?"; } } @@ -206,11 +207,37 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id, ss << "SKOLEM_FUN_" << id; Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags); d_skolemFuns[key] = k; + d_skolemFunMap[k] = key; return k; } return it->second; } +Node SkolemManager::mkSkolemFunction(SkolemFunId id, + TypeNode tn, + const std::vector<Node>& cacheVals, + int flags) +{ + Assert(cacheVals.size() > 1); + Node cacheVal = NodeManager::currentNM()->mkNode(SEXPR, cacheVals); + return mkSkolemFunction(id, tn, cacheVal, flags); +} + +bool SkolemManager::isSkolemFunction(Node k, + SkolemFunId& id, + Node& cacheVal) const +{ + std::map<Node, std::tuple<SkolemFunId, TypeNode, Node>>::const_iterator it = + d_skolemFunMap.find(k); + if (it == d_skolemFunMap.end()) + { + return false; + } + id = std::get<0>(it->second); + cacheVal = std::get<2>(it->second); + return true; +} + Node SkolemManager::mkDummySkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index d62153941..a7d35d155 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -29,6 +29,7 @@ class ProofGenerator; /** Skolem function identifier */ enum class SkolemFunId { + NONE, /** an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */ DIV_BY_ZERO, /** an uninterpreted function f s.t. f(x) = x / 0 (integer division) */ @@ -43,6 +44,13 @@ enum class SkolemFunId SHARED_SELECTOR, /** an application of seq.nth that is out of bounds */ SEQ_NTH_OOB, + /** + * Regular expression unfold component: if (str.in_re t R), where R is + * (re.++ r0 ... rn), then the RE_UNFOLD_POS_COMPONENT{t,R,i} is a string + * skolem ki such that t = (str.++ k0 ... kn) and (str.in_re k0 r0) for + * i = 0, ..., n. + */ + RE_UNFOLD_POS_COMPONENT, }; /** Converts a skolem function name to a string. */ const char* toString(SkolemFunId id); @@ -235,6 +243,16 @@ class SkolemManager TypeNode tn, Node cacheVal = Node::null(), int flags = NodeManager::SKOLEM_DEFAULT); + /** Same as above, with multiple cache values */ + Node mkSkolemFunction(SkolemFunId id, + TypeNode tn, + const std::vector<Node>& cacheVals, + int flags = NodeManager::SKOLEM_DEFAULT); + /** + * Is k a skolem function? Returns true if k was generated by the above call. + * Updates the arguments to the values used when constructing it. + */ + bool isSkolemFunction(Node k, SkolemFunId& id, Node& cacheVal) const; /** * Create a skolem constant with the given name, type, and comment. This * should only be used if the definition of the skolem does not matter. @@ -281,10 +299,10 @@ class SkolemManager static Node getOriginalForm(Node n); private: - /** - * Cached of skolem functions for mkSkolemFunction above. - */ + /** Cache of skolem functions for mkSkolemFunction above. */ std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node> d_skolemFuns; + /** Backwards mapping of above */ + std::map<Node, std::tuple<SkolemFunId, TypeNode, Node>> d_skolemFunMap; /** * Mapping from witness terms to proof generators. */ diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index b6f5a5c1b..4f3f91ba5 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -68,3 +68,41 @@ name = "Decision Heuristics" name = "sum" [[option.mode.USR1]] name = "usr1" + +[[option]] + name = "jhSkolemMode" + category = "expert" + long = "jh-skolem=MODE" + type = "JutificationSkolemMode" + default = "FIRST" + help = "policy for when to satisfy skolem definitions in justification heuristic" + help_mode = "Policy for when to satisfy skolem definitions in justification heuristic" +[[option.mode.FIRST]] + name = "first" + help = "satisfy pending relevant skolem definitions before input assertions" +[[option.mode.LAST]] + name = "last" + help = "satisfy pending relevant skolem definitions after input assertions" + +[[option]] + name = "jhRlvOrder" + category = "expert" + long = "jh-rlv-order" + type = "bool" + default = "false" + help = "maintain activity-based ordering for decision justification heuristic" + +[[option]] + name = "jhSkolemRlvMode" + category = "expert" + long = "jh-skolem-rlv=MODE" + type = "JutificationSkolemRlvMode" + default = "ASSERT" + help = "policy for when to consider skolem definitions relevant in justification heuristic" + help_mode = "Policy for when to consider skolem definitions relevant in justification heuristic" +[[option.mode.ASSERT]] + name = "assert" + help = "skolems are relevant when they occur in an asserted literal" +[[option.mode.ALWAYS]] + name = "always" + help = "skolems are always relevant" diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 2f3a49ac2..5542cfcf3 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -18,7 +18,7 @@ #include "expr/node_manager.h" #include "options/smt_options.h" -#include "expr/lazy_proof.h" +#include "proof/lazy_proof.h" #include "smt/preprocess_proof_generator.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index bb8e594d7..af88d5164 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -22,7 +22,7 @@ #include <vector> #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 7f6106e3a..de16cc49a 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -21,7 +21,7 @@ #include "context/cdlist.h" #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index 729252dd6..2312c38ed 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.h +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace preprocessing { diff --git a/src/expr/buffered_proof_generator.cpp b/src/proof/buffered_proof_generator.cpp index 2cbbd7e91..d6f54fb34 100644 --- a/src/expr/buffered_proof_generator.cpp +++ b/src/proof/buffered_proof_generator.cpp @@ -13,10 +13,10 @@ * Implementation of a proof generator for buffered proof steps. */ -#include "expr/buffered_proof_generator.h" +#include "proof/buffered_proof_generator.h" -#include "expr/proof.h" -#include "expr/proof_node_manager.h" +#include "proof/proof.h" +#include "proof/proof_node_manager.h" namespace cvc5 { diff --git a/src/expr/buffered_proof_generator.h b/src/proof/buffered_proof_generator.h index 2e1ef6c53..9d13faff4 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/proof/buffered_proof_generator.h @@ -15,11 +15,11 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H -#define CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H +#define CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H #include "context/cdhashmap.h" -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" namespace cvc5 { @@ -28,8 +28,8 @@ class ProofStep; /** * The proof generator for buffered steps. This class is a context-dependent - * mapping from formulas to proof steps. It does not generate ProofNodes until it - * is asked to provide a proof for a given fact. + * mapping from formulas to proof steps. It does not generate ProofNodes until + * it is asked to provide a proof for a given fact. */ class BufferedProofGenerator : public ProofGenerator { @@ -61,4 +61,4 @@ class BufferedProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H */ diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/proof/conv_proof_generator.cpp index 0e0ed3165..3635f3dea 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/proof/conv_proof_generator.cpp @@ -13,15 +13,15 @@ * Implementation of term conversion proof generator utility. */ -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" #include <sstream> -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" #include "expr/term_context.h" #include "expr/term_context_stack.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" using namespace cvc5::kind; @@ -232,7 +232,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f) } std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f); Trace("tconv-pf-gen") << "... success" << std::endl; - Assert (pfn!=nullptr); + Assert(pfn != nullptr); Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl; return pfn; } diff --git a/src/expr/term_conversion_proof_generator.h b/src/proof/conv_proof_generator.h index 70e606db4..f23a661ae 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/proof/conv_proof_generator.h @@ -15,12 +15,12 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H -#define CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__CONV_PROOF_GENERATOR_H +#define CVC5__PROOF__CONV_PROOF_GENERATOR_H #include "context/cdhashmap.h" -#include "expr/lazy_proof.h" -#include "expr/proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/proof_generator.h" namespace cvc5 { @@ -174,7 +174,7 @@ class TConvProofGenerator : public ProofGenerator uint32_t tctx = 0); /** Has rewrite step for term t */ bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const; - /** + /** * Get rewrite step for term t, returns the s provided in a call to * addRewriteStep if one exists, or null otherwise. */ @@ -253,4 +253,4 @@ class TConvProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__CONV_PROOF_GENERATOR_H */ diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/proof/conv_seq_proof_generator.cpp index 00e961628..65a7e462b 100644 --- a/src/expr/tconv_seq_proof_generator.cpp +++ b/src/proof/conv_seq_proof_generator.cpp @@ -13,11 +13,11 @@ * Term conversion sequence proof generator utility. */ -#include "expr/tconv_seq_proof_generator.h" +#include "proof/conv_seq_proof_generator.h" #include <sstream> -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" namespace cvc5 { diff --git a/src/expr/tconv_seq_proof_generator.h b/src/proof/conv_seq_proof_generator.h index bc067f60a..8d4417134 100644 --- a/src/expr/tconv_seq_proof_generator.h +++ b/src/proof/conv_seq_proof_generator.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H -#define CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H +#define CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" -#include "theory/trust_node.h" +#include "proof/proof_generator.h" +#include "proof/trust_node.h" namespace cvc5 { @@ -86,7 +86,7 @@ class TConvSeqProofGenerator : public ProofGenerator * generator, or one of the component proof generators, if only one step * rewrote. In the former case, all steps are registered to this class. * Using a component generator is an optimization that saves having to - * save the conversion steps or use this class. For example, if we have 2 + * save the conversion steps or use this class. For example, if we have 2 * term conversion components, and call this method on: * { a, b, c } * then this method calls: @@ -118,4 +118,4 @@ class TConvSeqProofGenerator : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H */ diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index 4ba409d6d..ca85aadd3 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -17,9 +17,9 @@ #include <sstream> -#include "expr/proof_checker.h" -#include "expr/proof_node_manager.h" #include "printer/smt2/smt2_printer.h" +#include "proof/proof_checker.h" +#include "proof/proof_node_manager.h" #include "theory/builtin/proof_checker.h" namespace cvc5 { diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index 6e6785080..0027d145a 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -20,7 +20,7 @@ #include <iostream> -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { namespace proof { diff --git a/src/theory/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp index c9a8823aa..34ff4fa75 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/proof/eager_proof_generator.cpp @@ -13,11 +13,11 @@ * Implementation of the abstract proof generator class. */ -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" -#include "expr/proof.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { @@ -122,8 +122,9 @@ TrustNode EagerProofGenerator::mkTrustNode(Node conc, return mkTrustNode(pfs->getResult(), pfs, isConflict); } -TrustNode EagerProofGenerator::mkTrustedRewrite( - Node a, Node b, std::shared_ptr<ProofNode> pf) +TrustNode EagerProofGenerator::mkTrustedRewrite(Node a, + Node b, + std::shared_ptr<ProofNode> pf) { if (pf == nullptr) { diff --git a/src/theory/eager_proof_generator.h b/src/proof/eager_proof_generator.h index c0b368e6e..ada48d893 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/proof/eager_proof_generator.h @@ -15,14 +15,14 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__EAGER_PROOF_GENERATOR_H -#define CVC5__THEORY__EAGER_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__EAGER_PROOF_GENERATOR_H +#define CVC5__PROOF__EAGER_PROOF_GENERATOR_H #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_rule.h" -#include "theory/trust_node.h" +#include "proof/proof_generator.h" +#include "proof/proof_rule.h" +#include "proof/trust_node.h" namespace cvc5 { @@ -159,8 +159,7 @@ class EagerProofGenerator : public ProofGenerator * @return The trust node corresponding to the fact that this generator has * a proof of a = b */ - TrustNode mkTrustedRewrite( - Node a, Node b, std::shared_ptr<ProofNode> pf); + TrustNode mkTrustedRewrite(Node a, Node b, std::shared_ptr<ProofNode> pf); //--------------------------------------- common proofs /** * This returns the trust node corresponding to the splitting lemma @@ -195,4 +194,4 @@ class EagerProofGenerator : public ProofGenerator } // namespace theory } // namespace cvc5 -#endif /* CVC5__THEORY__PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__PROOF_GENERATOR_H */ diff --git a/src/expr/lazy_proof.cpp b/src/proof/lazy_proof.cpp index 8a54637fa..d7b62a8dc 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/proof/lazy_proof.cpp @@ -13,11 +13,11 @@ * Implementation of lazy proof utility. */ -#include "expr/lazy_proof.h" +#include "proof/lazy_proof.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" using namespace cvc5::kind; @@ -178,8 +178,7 @@ void LazyCDProof::addLazyStep(Node expected, } } -ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, - bool& isSym) +ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, bool& isSym) { isSym = false; NodeProofGeneratorMap::const_iterator it = d_gens.find(fact); diff --git a/src/expr/lazy_proof.h b/src/proof/lazy_proof.h index efcda94bd..b566e408e 100644 --- a/src/expr/lazy_proof.h +++ b/src/proof/lazy_proof.h @@ -15,10 +15,10 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__LAZY_PROOF_H -#define CVC5__EXPR__LAZY_PROOF_H +#ifndef CVC5__PROOF__LAZY_PROOF_H +#define CVC5__PROOF__LAZY_PROOF_H -#include "expr/proof.h" +#include "proof/proof.h" namespace cvc5 { @@ -107,4 +107,4 @@ class LazyCDProof : public CDProof } // namespace cvc5 -#endif /* CVC5__EXPR__LAZY_PROOF_H */ +#endif /* CVC5__PROOF__LAZY_PROOF_H */ diff --git a/src/expr/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp index 3ce2212be..4c1b19ffe 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/proof/lazy_proof_chain.cpp @@ -13,14 +13,14 @@ * Implementation of lazy proof utility. */ -#include "expr/lazy_proof_chain.h" +#include "proof/lazy_proof_chain.h" -#include "expr/proof.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/proof_options.h" +#include "proof/proof.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" namespace cvc5 { diff --git a/src/expr/lazy_proof_chain.h b/src/proof/lazy_proof_chain.h index 1abb3f84e..4315ee87a 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/proof/lazy_proof_chain.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__LAZY_PROOF_CHAIN_H -#define CVC5__EXPR__LAZY_PROOF_CHAIN_H +#ifndef CVC5__PROOF__LAZY_PROOF_CHAIN_H +#define CVC5__PROOF__LAZY_PROOF_CHAIN_H #include <vector> #include "context/cdhashmap.h" -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" namespace cvc5 { @@ -151,4 +151,4 @@ class LazyCDProofChain : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__LAZY_PROOF_CHAIN_H */ +#endif /* CVC5__PROOF__LAZY_PROOF_CHAIN_H */ diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp index 3fd3795c1..a50b9efd4 100644 --- a/src/theory/lazy_tree_proof_generator.cpp +++ b/src/proof/lazy_tree_proof_generator.cpp @@ -13,14 +13,14 @@ * Implementation of the lazy tree proof generator class. */ -#include "theory/lazy_tree_proof_generator.h" +#include "proof/lazy_tree_proof_generator.h" #include <iostream> #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { diff --git a/src/theory/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h index 7ab921a70..8b8d344e9 100644 --- a/src/theory/lazy_tree_proof_generator.h +++ b/src/proof/lazy_tree_proof_generator.h @@ -15,14 +15,14 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H -#define CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H +#ifndef CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H +#define CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H #include <iostream> #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { diff --git a/src/expr/proof.cpp b/src/proof/proof.cpp index 289a5be5b..a100be990 100644 --- a/src/expr/proof.cpp +++ b/src/proof/proof.cpp @@ -13,11 +13,11 @@ * Implementation of proof. */ -#include "expr/proof.h" +#include "proof/proof.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" using namespace cvc5::kind; diff --git a/src/expr/proof.h b/src/proof/proof.h index 496815938..2c57e0a2e 100644 --- a/src/expr/proof.h +++ b/src/proof/proof.h @@ -15,15 +15,15 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_H -#define CVC5__EXPR__PROOF_H +#ifndef CVC5__PROOF__PROOF_H +#define CVC5__PROOF__PROOF_H #include <vector> #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_step_buffer.h" +#include "proof/proof_generator.h" +#include "proof/proof_step_buffer.h" namespace cvc5 { @@ -275,4 +275,4 @@ class CDProof : public ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_MANAGER_H */ +#endif /* CVC5__PROOF__PROOF_MANAGER_H */ diff --git a/src/expr/proof_checker.cpp b/src/proof/proof_checker.cpp index 69f880ed5..7a2e5293e 100644 --- a/src/expr/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -13,11 +13,11 @@ * Implementation of proof checker. */ -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" -#include "expr/proof_node.h" #include "expr/skolem_manager.h" #include "options/proof_options.h" +#include "proof/proof_node.h" #include "smt/smt_statistics_registry.h" using namespace cvc5::kind; @@ -78,7 +78,7 @@ Node ProofRuleChecker::mkKindNode(Kind k) ProofCheckerStatistics::ProofCheckerStatistics() : d_ruleChecks(smtStatisticsRegistry().registerHistogram<PfRule>( - "ProofCheckerStatistics::ruleChecks")), + "ProofCheckerStatistics::ruleChecks")), d_totalRuleChecks(smtStatisticsRegistry().registerInt( "ProofCheckerStatistics::totalRuleChecks")) { diff --git a/src/expr/proof_checker.h b/src/proof/proof_checker.h index e778f687e..ac5531bf4 100644 --- a/src/expr/proof_checker.h +++ b/src/proof/proof_checker.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_CHECKER_H -#define CVC5__EXPR__PROOF_CHECKER_H +#ifndef CVC5__PROOF__PROOF_CHECKER_H +#define CVC5__PROOF__PROOF_CHECKER_H #include <map> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" #include "util/statistics_stats.h" namespace cvc5 { @@ -203,4 +203,4 @@ class ProofChecker } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_CHECKER_H */ +#endif /* CVC5__PROOF__PROOF_CHECKER_H */ diff --git a/src/expr/proof_ensure_closed.cpp b/src/proof/proof_ensure_closed.cpp index e89bd6692..774b25ef6 100644 --- a/src/expr/proof_ensure_closed.cpp +++ b/src/proof/proof_ensure_closed.cpp @@ -13,15 +13,15 @@ * Implementation of debug checks for ensuring proofs are closed. */ -#include "expr/proof_ensure_closed.h" +#include "proof/proof_ensure_closed.h" #include <sstream> -#include "expr/proof_generator.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" #include "options/proof_options.h" #include "options/smt_options.h" +#include "proof/proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" namespace cvc5 { diff --git a/src/expr/proof_ensure_closed.h b/src/proof/proof_ensure_closed.h index 3d126a4a1..cacfeeeed 100644 --- a/src/expr/proof_ensure_closed.h +++ b/src/proof/proof_ensure_closed.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_ENSURE_CLOSED_H -#define CVC5__EXPR__PROOF_ENSURE_CLOSED_H +#ifndef CVC5__PROOF__PROOF_ENSURE_CLOSED_H +#define CVC5__PROOF__PROOF_ENSURE_CLOSED_H #include "expr/node.h" @@ -70,4 +70,4 @@ void pfnEnsureClosedWrt(ProofNode* pn, const char* ctx); } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_ENSURE_CLOSED_H */ +#endif /* CVC5__PROOF__PROOF_ENSURE_CLOSED_H */ diff --git a/src/expr/proof_generator.cpp b/src/proof/proof_generator.cpp index 7c034c10d..bbfde7986 100644 --- a/src/expr/proof_generator.cpp +++ b/src/proof/proof_generator.cpp @@ -13,14 +13,14 @@ * Implementation of proof generator utility. */ -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" #include <sstream> -#include "expr/proof.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" #include "options/smt_options.h" +#include "proof/proof.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" namespace cvc5 { diff --git a/src/expr/proof_generator.h b/src/proof/proof_generator.h index 2e87ab756..a8fe43909 100644 --- a/src/expr/proof_generator.h +++ b/src/proof/proof_generator.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_GENERATOR_H -#define CVC5__EXPR__PROOF_GENERATOR_H +#ifndef CVC5__PROOF__PROOF_GENERATOR_H +#define CVC5__PROOF__PROOF_GENERATOR_H #include "expr/node.h" @@ -110,4 +110,4 @@ class ProofGenerator } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_GENERATOR_H */ +#endif /* CVC5__PROOF__PROOF_GENERATOR_H */ diff --git a/src/expr/proof_node.cpp b/src/proof/proof_node.cpp index 92daad8ed..e3affb306 100644 --- a/src/expr/proof_node.cpp +++ b/src/proof/proof_node.cpp @@ -13,10 +13,10 @@ * Implementation of proof node utility. */ -#include "expr/proof_node.h" +#include "proof/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_to_sexpr.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_to_sexpr.h" namespace cvc5 { diff --git a/src/expr/proof_node.h b/src/proof/proof_node.h index f8d71f703..db82cc63d 100644 --- a/src/expr/proof_node.h +++ b/src/proof/proof_node.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_H -#define CVC5__EXPR__PROOF_NODE_H +#ifndef CVC5__PROOF__PROOF_NODE_H +#define CVC5__PROOF__PROOF_NODE_H #include <vector> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { @@ -142,4 +142,4 @@ std::ostream& operator<<(std::ostream& out, const ProofNode& pn); } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_NODE_H */ +#endif /* CVC5__PROOF__PROOF_NODE_H */ diff --git a/src/expr/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp index 4bb35b5dc..82ccc034f 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/proof/proof_node_algorithm.cpp @@ -13,9 +13,9 @@ * Implementation of proof node algorithm utilities. */ -#include "expr/proof_node_algorithm.h" +#include "proof/proof_node_algorithm.h" -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { namespace expr { diff --git a/src/expr/proof_node_algorithm.h b/src/proof/proof_node_algorithm.h index 4c89dd4bc..1ccefb0a2 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/proof/proof_node_algorithm.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_ALGORITHM_H -#define CVC5__EXPR__PROOF_NODE_ALGORITHM_H +#ifndef CVC5__PROOF__PROOF_NODE_ALGORITHM_H +#define CVC5__PROOF__PROOF_NODE_ALGORITHM_H #include <vector> @@ -73,4 +73,4 @@ bool containsSubproof(ProofNode* pn, } // namespace expr } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_NODE_ALGORITHM_H */ +#endif /* CVC5__PROOF__PROOF_NODE_ALGORITHM_H */ diff --git a/src/expr/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index c2c72f35d..cf19eebdf 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -13,23 +13,22 @@ * Implementation of proof node manager. */ -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include <sstream> -#include "expr/proof.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" #include "options/proof_options.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" #include "theory/rewriter.h" using namespace cvc5::kind; namespace cvc5 { -ProofNodeManager::ProofNodeManager(ProofChecker* pc) - : d_checker(pc) +ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) { d_true = NodeManager::currentNM()->mkConst(true); } diff --git a/src/expr/proof_node_manager.h b/src/proof/proof_node_manager.h index 853d22de7..2fa7ed3e9 100644 --- a/src/expr/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_MANAGER_H -#define CVC5__EXPR__PROOF_NODE_MANAGER_H +#ifndef CVC5__PROOF__PROOF_NODE_MANAGER_H +#define CVC5__PROOF__PROOF_NODE_MANAGER_H #include <vector> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { @@ -203,4 +203,4 @@ class ProofNodeManager } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_NODE_H */ +#endif /* CVC5__PROOF__PROOF_NODE_H */ diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp index 033232959..85fc2395e 100644 --- a/src/expr/proof_node_to_sexpr.cpp +++ b/src/proof/proof_node_to_sexpr.cpp @@ -13,13 +13,13 @@ * Implementation of proof node to s-expression. */ -#include "expr/proof_node_to_sexpr.h" +#include "proof/proof_node_to_sexpr.h" #include <iostream> #include <sstream> -#include "expr/proof_node.h" #include "options/proof_options.h" +#include "proof/proof_node.h" using namespace cvc5::kind; diff --git a/src/expr/proof_node_to_sexpr.h b/src/proof/proof_node_to_sexpr.h index d4cca8eae..c358f3445 100644 --- a/src/expr/proof_node_to_sexpr.h +++ b/src/proof/proof_node_to_sexpr.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_TO_SEXPR_H -#define CVC5__EXPR__PROOF_NODE_TO_SEXPR_H +#ifndef CVC5__PROOF__PROOF_NODE_TO_SEXPR_H +#define CVC5__PROOF__PROOF_NODE_TO_SEXPR_H #include <map> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { @@ -67,4 +67,4 @@ class ProofNodeToSExpr } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_RULE_H */ +#endif /* CVC5__PROOF__PROOF_RULE_H */ diff --git a/src/expr/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp index e2fd0c566..2bdb54a45 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/proof/proof_node_updater.cpp @@ -13,12 +13,12 @@ * Implementation of a utility for updating proof nodes. */ -#include "expr/proof_node_updater.h" +#include "proof/proof_node_updater.h" -#include "expr/lazy_proof.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_manager.h" +#include "proof/lazy_proof.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" namespace cvc5 { diff --git a/src/expr/proof_node_updater.h b/src/proof/proof_node_updater.h index 215c61210..6b8841e67 100644 --- a/src/expr/proof_node_updater.h +++ b/src/proof/proof_node_updater.h @@ -15,14 +15,14 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_NODE_UPDATER_H -#define CVC5__EXPR__PROOF_NODE_UPDATER_H +#ifndef CVC5__PROOF__PROOF_NODE_UPDATER_H +#define CVC5__PROOF__PROOF_NODE_UPDATER_H #include <map> #include <memory> #include "expr/node.h" -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { diff --git a/src/expr/proof_rule.cpp b/src/proof/proof_rule.cpp index f4e8078dc..0cefe1209 100644 --- a/src/expr/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -13,7 +13,7 @@ * Implementation of proof rule. */ -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" #include <iostream> diff --git a/src/expr/proof_rule.h b/src/proof/proof_rule.h index 9771dda31..107285cc3 100644 --- a/src/expr/proof_rule.h +++ b/src/proof/proof_rule.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_RULE_H -#define CVC5__EXPR__PROOF_RULE_H +#ifndef CVC5__PROOF__PROOF_RULE_H +#define CVC5__PROOF__PROOF_RULE_H #include <iosfwd> @@ -1450,4 +1450,4 @@ struct PfRuleHashFunction } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_RULE_H */ +#endif /* CVC5__PROOF__PROOF_RULE_H */ diff --git a/src/expr/proof_set.h b/src/proof/proof_set.h index 5ea9c1021..4015e0466 100644 --- a/src/expr/proof_set.h +++ b/src/proof/proof_set.h @@ -15,14 +15,14 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_SET_H -#define CVC5__EXPR__PROOF_SET_H +#ifndef CVC5__PROOF__PROOF_SET_H +#define CVC5__PROOF__PROOF_SET_H #include <memory> #include "context/cdlist.h" #include "context/context.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" namespace cvc5 { @@ -73,4 +73,4 @@ class CDProofSet } // namespace cvc5 -#endif /* CVC5__EXPR__LAZY_PROOF_SET_H */ +#endif /* CVC5__PROOF__LAZY_PROOF_SET_H */ diff --git a/src/expr/proof_step_buffer.cpp b/src/proof/proof_step_buffer.cpp index 84cfc040c..309802505 100644 --- a/src/expr/proof_step_buffer.cpp +++ b/src/proof/proof_step_buffer.cpp @@ -13,9 +13,9 @@ * Implementation of proof step and proof step buffer utilities. */ -#include "expr/proof_step_buffer.h" +#include "proof/proof_step_buffer.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" using namespace cvc5::kind; diff --git a/src/expr/proof_step_buffer.h b/src/proof/proof_step_buffer.h index b9350cf45..4c1bfa8a3 100644 --- a/src/expr/proof_step_buffer.h +++ b/src/proof/proof_step_buffer.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__EXPR__PROOF_STEP_BUFFER_H -#define CVC5__EXPR__PROOF_STEP_BUFFER_H +#ifndef CVC5__PROOF__PROOF_STEP_BUFFER_H +#define CVC5__PROOF__PROOF_STEP_BUFFER_H #include <vector> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { @@ -95,4 +95,4 @@ class ProofStepBuffer } // namespace cvc5 -#endif /* CVC5__EXPR__PROOF_STEP_BUFFER_H */ +#endif /* CVC5__PROOF__PROOF_STEP_BUFFER_H */ diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/proof/theory_proof_step_buffer.cpp index 667c8d114..f00c664c8 100644 --- a/src/theory/theory_proof_step_buffer.cpp +++ b/src/proof/theory_proof_step_buffer.cpp @@ -13,9 +13,9 @@ * Implementation of theory proof step buffer utility. */ -#include "theory/theory_proof_step_buffer.h" +#include "proof/theory_proof_step_buffer.h" -#include "expr/proof.h" +#include "proof/proof.h" using namespace cvc5::kind; diff --git a/src/theory/theory_proof_step_buffer.h b/src/proof/theory_proof_step_buffer.h index 1832ddb08..fc2e25e5a 100644 --- a/src/theory/theory_proof_step_buffer.h +++ b/src/proof/theory_proof_step_buffer.h @@ -15,13 +15,13 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H -#define CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H +#ifndef CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H +#define CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H #include <vector> #include "expr/node.h" -#include "expr/proof_step_buffer.h" +#include "proof/proof_step_buffer.h" #include "theory/builtin/proof_checker.h" namespace cvc5 { @@ -117,4 +117,4 @@ class TheoryProofStepBuffer : public ProofStepBuffer } // namespace theory } // namespace cvc5 -#endif /* CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H */ +#endif /* CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H */ diff --git a/src/theory/trust_node.cpp b/src/proof/trust_node.cpp index 4086d6e86..d99e6de51 100644 --- a/src/theory/trust_node.cpp +++ b/src/proof/trust_node.cpp @@ -13,10 +13,10 @@ * Implementation of the trust node utility. */ -#include "theory/trust_node.h" +#include "proof/trust_node.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_generator.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_generator.h" namespace cvc5 { namespace theory { diff --git a/src/theory/trust_node.h b/src/proof/trust_node.h index 0a4f20c34..200dececd 100644 --- a/src/theory/trust_node.h +++ b/src/proof/trust_node.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__TRUST_NODE_H -#define CVC5__THEORY__TRUST_NODE_H +#ifndef CVC5__PROOF__TRUST_NODE_H +#define CVC5__PROOF__TRUST_NODE_H #include "expr/node.h" @@ -75,8 +75,8 @@ std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk); * provided, is capable of proving the given conflict or lemma, or an assertion * failure occurs. Otherwise an assertion error is given. * - * While this is not enforced, a `TrustNode` generally encapsulates a **closed** proof - * of the formula: one without free assumptions. + * While this is not enforced, a `TrustNode` generally encapsulates a **closed** + * proof of the formula: one without free assumptions. */ class TrustNode { @@ -175,4 +175,4 @@ std::ostream& operator<<(std::ostream& out, TrustNode n); } // namespace theory } // namespace cvc5 -#endif /* CVC5__THEORY__TRUST_NODE_H */ +#endif /* CVC5__PROOF__TRUST_NODE_H */ diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index bed637904..d0f5006e1 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -27,8 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/output.h" #include "context/context.h" #include "cvc5_private.h" -#include "expr/proof_node_manager.h" #include "proof/clause_id.h" +#include "proof/proof_node_manager.h" #include "prop/minisat/core/SolverTypes.h" #include "prop/minisat/mtl/Alg.h" #include "prop/minisat/mtl/Heap.h" diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 708441b0c..97abdb077 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -19,14 +19,14 @@ #define CVC5__PROP__PROOF_CNF_STREAM_H #include "context/cdhashmap.h" -#include "expr/lazy_proof.h" #include "expr/node.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/eager_proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" +#include "proof/theory_proof_step_buffer.h" #include "prop/cnf_stream.h" #include "prop/sat_proof_manager.h" -#include "theory/eager_proof_generator.h" -#include "theory/theory_proof_step_buffer.h" namespace cvc5 { namespace prop { diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h index b4a8d1b17..0065ed99e 100644 --- a/src/prop/proof_post_processor.h +++ b/src/prop/proof_post_processor.h @@ -21,7 +21,7 @@ #include <map> #include <unordered_set> -#include "expr/proof_node_updater.h" +#include "proof/proof_node_updater.h" #include "prop/proof_cnf_stream.h" namespace cvc5 { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index a12816906..8903d4bc3 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -22,9 +22,9 @@ #include "context/cdlist.h" #include "expr/node.h" +#include "proof/trust_node.h" #include "prop/skolem_def_manager.h" #include "theory/output_channel.h" -#include "theory/trust_node.h" #include "util/result.h" namespace cvc5 { diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index 000cebb72..09c5fb915 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -15,8 +15,8 @@ #include "prop/prop_proof_manager.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node_algorithm.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node_algorithm.h" #include "prop/prop_proof_manager.h" #include "prop/sat_solver.h" diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index 1374acf8d..e415ed441 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -19,8 +19,8 @@ #define CVC5__PROP_PROOF_MANAGER_H #include "context/cdlist.h" -#include "expr/proof.h" -#include "expr/proof_node_manager.h" +#include "proof/proof.h" +#include "proof/proof_node_manager.h" #include "prop/proof_post_processor.h" #include "prop/sat_proof_manager.h" diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 60a4c9704..5bec41e2b 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -15,11 +15,11 @@ #include "prop/sat_proof_manager.h" -#include "expr/proof_node_algorithm.h" #include "options/proof_options.h" +#include "proof/proof_node_algorithm.h" +#include "proof/theory_proof_step_buffer.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" -#include "theory/theory_proof_step_buffer.h" namespace cvc5 { namespace prop { diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index a53f66cec..a224f3a28 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -19,9 +19,9 @@ #define CVC5__SAT_PROOF_MANAGER_H #include "context/cdhashset.h" -#include "expr/buffered_proof_generator.h" -#include "expr/lazy_proof_chain.h" #include "expr/node.h" +#include "proof/buffered_proof_generator.h" +#include "proof/lazy_proof_chain.h" #include "prop/minisat/core/SolverTypes.h" #include "prop/sat_solver_types.h" diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 963810594..9ad54e292 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -23,8 +23,8 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/node.h" -#include "expr/proof_node_manager.h" #include "proof/clause_id.h" +#include "proof/proof_node_manager.h" #include "prop/bv_sat_solver_notify.h" #include "prop/sat_solver_types.h" #include "util/statistics_stats.h" diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index afd99ae83..d6ae1f975 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -26,11 +26,11 @@ #include "context/cdqueue.h" #include "expr/node.h" +#include "proof/trust_node.h" #include "prop/registrar.h" #include "prop/sat_solver_types.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" -#include "theory/trust_node.h" #include "util/resource_manager.h" namespace cvc5 { diff --git a/src/smt/env.cpp b/src/smt/env.cpp index f9e2a8458..647981ab3 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -18,9 +18,9 @@ #include "context/context.h" #include "expr/node.h" -#include "expr/term_conversion_proof_generator.h" #include "options/base_options.h" #include "printer/printer.h" +#include "proof/conv_proof_generator.h" #include "smt/dump_manager.h" #include "smt/smt_engine_stats.h" #include "theory/rewriter.h" diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 91287e5f9..293c46906 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -19,8 +19,8 @@ #include <utility> #include "expr/node_manager_attributes.h" -#include "expr/term_conversion_proof_generator.h" #include "preprocessing/assertion_pipeline.h" +#include "proof/conv_proof_generator.h" #include "smt/env.h" #include "smt/smt_engine.h" #include "smt/smt_engine_stats.h" diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index 801622e27..ba89a1063 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -21,7 +21,7 @@ #include <unordered_map> #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 3ae03e58f..3f657db63 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -18,10 +18,10 @@ #include <sstream> -#include "expr/proof.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" #include "options/proof_options.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index 140a7c91a..347f4af3b 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -19,11 +19,11 @@ #define CVC5__SMT__PREPROCESS_PROOF_GENERATOR_H #include "context/cdhashmap.h" -#include "expr/lazy_proof.h" -#include "expr/proof.h" -#include "expr/proof_set.h" -#include "expr/proof_generator.h" -#include "theory/trust_node.h" +#include "proof/lazy_proof.h" +#include "proof/proof.h" +#include "proof/proof_generator.h" +#include "proof/proof_set.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 0968aa1f9..ad1e40c77 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -15,13 +15,13 @@ #include "smt/proof_manager.h" -#include "expr/proof_checker.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/base_options.h" #include "options/proof_options.h" #include "options/smt_options.h" #include "proof/dot/dot_printer.h" +#include "proof/proof_checker.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" #include "smt/assertions.h" #include "smt/preprocess_proof_generator.h" #include "smt/proof_post_processor.h" diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index f98d1d727..62e18c3b2 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -15,11 +15,11 @@ #include "smt/proof_post_processor.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/proof_options.h" #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" +#include "proof/proof_node_manager.h" #include "smt/smt_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/builtin/proof_checker.h" diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 72fa3581d..f9e93fa91 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -22,7 +22,7 @@ #include <sstream> #include <unordered_set> -#include "expr/proof_node_updater.h" +#include "proof/proof_node_updater.h" #include "smt/witness_form.h" #include "util/statistics_stats.h" diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index eaf5cf82f..3bb998688 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -17,12 +17,12 @@ #include <vector> #include "expr/attribute.h" -#include "expr/lazy_proof.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/term_context_stack.h" -#include "expr/term_conversion_proof_generator.h" #include "options/smt_options.h" +#include "proof/conv_proof_generator.h" +#include "proof/lazy_proof.h" using namespace std; diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 6a3a1c019..c2b1f27f3 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -24,7 +24,7 @@ #include "context/context.h" #include "expr/node.h" #include "expr/term_context.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" #include "util/hash.h" namespace cvc5 { diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index df8f2f9d9..ba2c07326 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -15,7 +15,7 @@ #include "unsat_core_manager.h" -#include "expr/proof_node_algorithm.h" +#include "proof/proof_node_algorithm.h" #include "smt/assertions.h" namespace cvc5 { diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h index dcd246f2e..e064b83a7 100644 --- a/src/smt/unsat_core_manager.h +++ b/src/smt/unsat_core_manager.h @@ -20,7 +20,7 @@ #include "context/cdlist.h" #include "expr/node.h" -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 980cbcadb..8522d41f0 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -20,9 +20,9 @@ #include <unordered_set> -#include "expr/proof.h" -#include "expr/proof_generator.h" -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" +#include "proof/proof.h" +#include "proof/proof_generator.h" namespace cvc5 { namespace smt { diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index f343ce56a..33860d2d9 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -25,12 +25,12 @@ #include "base/cvc5config.h" #include "base/output.h" +#include "proof/eager_proof_generator.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/cut_log.h" #include "theory/arith/matrix.h" #include "theory/arith/normal_form.h" -#include "theory/eager_proof_generator.h" #ifdef CVC5_USE_GLPK #include "theory/arith/partial_model.h" diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 2edc7b210..0c0a4959d 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -18,8 +18,8 @@ #include "theory/arith/callbacks.h" -#include "expr/proof_node.h" #include "expr/skolem_manager.h" +#include "proof/proof_node.h" #include "theory/arith/proof_macros.h" #include "theory/arith/theory_arith_private.h" diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 3d5e7270b..96272f939 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -19,8 +19,9 @@ #include "theory/arith/congruence_manager.h" #include "base/output.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "options/arith_options.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/constraint.h" @@ -29,7 +30,6 @@ #include "theory/rewriter.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" -#include "options/arith_options.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index e45b7bf29..8ada48cfe 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -24,11 +24,11 @@ #include "context/cdlist.h" #include "context/cdmaybe.h" #include "context/cdtrail_queue.h" +#include "proof/trust_node.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" -#include "theory/trust_node.h" #include "theory/uf/equality_engine_notify.h" #include "util/dense_map.h" #include "util/statistics_stats.h" diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 15dfe4791..d8fc1c578 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -22,16 +22,15 @@ #include <unordered_set> #include "base/output.h" -#include "expr/proof_node_manager.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node_manager.h" #include "smt/smt_statistics_registry.h" -#include "theory/eager_proof_generator.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "theory/rewriter.h" - using namespace std; using namespace cvc5::kind; diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 0d3c96f89..fce071e6e 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -86,12 +86,12 @@ #include "context/cdlist.h" #include "context/cdqueue.h" #include "expr/node.h" +#include "proof/trust_node.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/delta_rational.h" #include "theory/arith/proof_macros.h" -#include "theory/trust_node.h" #include "util/statistics_stats.h" namespace cvc5 { diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index d7ce05b60..8cc544fc4 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index b0d785b2a..374a7e4ef 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -17,7 +17,7 @@ #ifdef CVC5_POLY_IMP -#include "theory/lazy_tree_proof_generator.h" +#include "proof/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" namespace cvc5 { diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index b493455a6..613db7565 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -25,9 +25,9 @@ #include <vector> #include "expr/node.h" -#include "expr/proof_set.h" +#include "proof/lazy_tree_proof_generator.h" +#include "proof/proof_set.h" #include "theory/arith/nl/cad/cdcac_utils.h" -#include "theory/lazy_tree_proof_generator.h" namespace cvc5 { diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 9ebd42d55..c1937797e 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -18,11 +18,11 @@ #include <vector> #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/monomial.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index b0a4fd859..7c2cc1b9b 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -19,7 +19,7 @@ #include <vector> #include "expr/node.h" -#include "expr/proof_set.h" +#include "proof/proof_set.h" #include "theory/arith/nl/ext/monomial.h" namespace cvc5 { diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index c4bba6ec8..d6b732eb9 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -16,12 +16,12 @@ #include "theory/arith/nl/ext/factoring_check.h" #include "expr/node.h" -#include "expr/proof.h" #include "expr/skolem_manager.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/ext/ext_state.h" +#include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 44f59c521..0deb2c99d 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -16,8 +16,8 @@ #include "theory/arith/nl/ext/monomial_bounds_check.h" #include "expr/node.h" -#include "expr/proof.h" #include "options/arith_options.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 404916453..bf38bc8f0 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -16,12 +16,12 @@ #include "theory/arith/nl/ext/monomial_check.h" #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" -#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/ext/ext_state.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h index 400126510..bf28cea59 100644 --- a/src/theory/arith/nl/ext/proof_checker.h +++ b/src/theory/arith/nl/ext/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index ace7e0868..6d9faa356 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -16,11 +16,11 @@ #include "theory/arith/nl/ext/split_zero_check.h" #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/ext/ext_state.h" +#include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index a66f1396c..9efa9c0f2 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -16,11 +16,11 @@ #include "theory/arith/nl/ext/tangent_plane_check.h" #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/ext/ext_state.h" +#include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 11e2b9cc8..73279a782 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -20,8 +20,8 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/proof.h" #include "options/arith_options.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h index 8675afe39..06359e62a 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.h +++ b/src/theory/arith/nl/transcendental/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 26d959878..6fdd4cc15 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -20,9 +20,9 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/proof.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index c0f5d23b2..db20713f1 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -15,7 +15,7 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 74f005294..56cbec79a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -17,7 +17,7 @@ #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H #include "expr/node.h" -#include "expr/proof_set.h" +#include "proof/proof_set.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/transcendental/proof_checker.h" #include "theory/arith/nl/transcendental/taylor_generator.h" diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index f39be2c59..7b4e920fb 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -19,8 +19,8 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" -#include "expr/term_conversion_proof_generator.h" #include "options/arith_options.h" +#include "proof/conv_proof_generator.h" #include "smt/logic_exception.h" #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 829601827..27a3d293e 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -19,7 +19,7 @@ #include "expr/node.h" #include "expr/skolem_manager.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h index 402656154..8fa9f21c1 100644 --- a/src/theory/arith/proof_checker.h +++ b/src/theory/arith/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__ARITH__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1843ddb8a..5c4678cb4 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -15,9 +15,9 @@ #include "theory/arith/theory_arith.h" -#include "expr/proof_checker.h" -#include "expr/proof_rule.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" +#include "proof/proof_rule.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/infer_bounds.h" diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 911954a5a..d12553e90 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -33,13 +33,13 @@ #include "expr/node.h" #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "expr/proof_rule.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() #include "preprocessing/util/ite_utilities.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" +#include "proof/proof_rule.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index e029e3c41..e3094ae88 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -28,6 +28,7 @@ #include "expr/kind.h" #include "expr/node.h" #include "expr/node_builder.h" +#include "proof/trust_node.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" @@ -47,7 +48,6 @@ #include "theory/arith/proof_checker.h" #include "theory/arith/soi_simplex.h" #include "theory/arith/theory_arith.h" -#include "theory/trust_node.h" #include "theory/valuation.h" #include "util/dense_map.h" #include "util/integer.h" diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index 93feb0a53..9b219c9b7 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H #include "expr/node.h" -#include "expr/proof_rule.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_rule.h" #include "theory/theory_inference_manager.h" namespace cvc5 { diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h index 9064dbfca..0b7bef163 100644 --- a/src/theory/arrays/proof_checker.h +++ b/src/theory/arrays/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__ARRAYS__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9b5676d65..0bdccfd17 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -20,9 +20,9 @@ #include "expr/kind.h" #include "expr/node_algorithm.h" -#include "expr/proof_checker.h" #include "options/arrays_options.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/arrays/skolem_cache.h" diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index d5917f91c..c2aa9eb1e 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -15,7 +15,7 @@ #include "theory/bags/theory_bags.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" #include "smt/logic_exception.h" #include "theory/bags/normal_form.h" #include "theory/rewriter.h" diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 7920f5b7f..2fa2890c2 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -20,10 +20,10 @@ #include <vector> #include "expr/node_algorithm.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "theory/booleans/proof_circuit_propagator.h" -#include "theory/eager_proof_generator.h" #include "theory/theory.h" #include "util/hash.h" #include "util/utility.h" diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 1d4f6e9ee..74e1a7cd8 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -26,9 +26,9 @@ #include "context/cdhashset.h" #include "context/cdo.h" #include "context/context.h" -#include "expr/lazy_proof_chain.h" #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/lazy_proof_chain.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h index 47a1ce633..114ab2e9b 100644 --- a/src/theory/booleans/proof_checker.h +++ b/src/theory/booleans/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__BOOLEANS__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index d1f8bb854..f7e788e9a 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -17,8 +17,8 @@ #include <sstream> -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h index 624a17f2f..0bed57078 100644 --- a/src/theory/booleans/proof_circuit_propagator.h +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -21,7 +21,7 @@ #include <memory> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index bac2be70c..3aac5ecfb 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -18,7 +18,7 @@ #include <stack> #include <vector> -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/booleans/theory_bool_rewriter.h" diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index dd6bf82e7..892fc7a4b 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" #include "theory/quantifiers/extended_rewrite.h" namespace cvc5 { diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index c5bd77e36..80c5dba3d 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -16,7 +16,7 @@ #include "theory/builtin/theory_builtin.h" #include "expr/kind.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index 6082a7128..a55adaace 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -16,8 +16,8 @@ #include <unordered_set> -#include "expr/term_conversion_proof_generator.h" #include "options/proof_options.h" +#include "proof/conv_proof_generator.h" #include "theory/theory_model.h" namespace cvc5 { diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 3da08f868..31d9443c8 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -21,12 +21,12 @@ #include <unordered_map> #include "context/cdqueue.h" +#include "proof/eager_proof_generator.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "theory/bv/bitblast/simple_bitblaster.h" #include "theory/bv/bv_solver.h" #include "theory/bv/proof_checker.h" -#include "theory/eager_proof_generator.h" namespace cvc5 { diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index 3faad29a9..a16bf7eb8 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -15,7 +15,7 @@ #include "theory/bv/bv_solver_simple.h" -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h index 674678ff8..c89dd359c 100644 --- a/src/theory/bv/proof_checker.h +++ b/src/theory/bv/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__BV__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" #include "theory/bv/bitblast/simple_bitblaster.h" namespace cvc5 { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c5ab08f0c..22b05b026 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -15,9 +15,9 @@ #include "theory/bv/theory_bv.h" -#include "expr/proof_checker.h" #include "options/bv_options.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/bv_solver_bitblast.h" #include "theory/bv/bv_solver_lazy.h" diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 33300ead8..2b35fb97d 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -16,8 +16,8 @@ #include "theory/combination_engine.h" #include "expr/node_visitor.h" +#include "proof/eager_proof_generator.h" #include "theory/care_graph.h" -#include "theory/eager_proof_generator.h" #include "theory/ee_manager_distributed.h" #include "theory/model_manager.h" #include "theory/model_manager_distributed.h" diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 5ab8a563f..19f396a56 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -15,8 +15,8 @@ #include "theory/datatypes/infer_proof_cons.h" -#include "expr/proof.h" -#include "expr/proof_checker.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/model_manager.h" #include "theory/rewriter.h" diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h index f8e7eea09..6c1663a09 100644 --- a/src/theory/datatypes/infer_proof_cons.h +++ b/src/theory/datatypes/infer_proof_cons.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" #include "theory/datatypes/inference.h" namespace cvc5 { diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h index db1d2b4b0..2dac0d7aa 100644 --- a/src/theory/datatypes/inference.h +++ b/src/theory/datatypes/inference.h @@ -19,9 +19,9 @@ #define CVC5__THEORY__DATATYPES__INFERENCE_H #include "expr/node.h" +#include "proof/trust_node.h" #include "theory/inference_id.h" #include "theory/theory_inference.h" -#include "theory/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 393813590..014255a7c 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -17,8 +17,8 @@ #include "expr/dtype.h" #include "options/datatypes_options.h" +#include "proof/eager_proof_generator.h" #include "smt/smt_statistics_registry.h" -#include "theory/eager_proof_generator.h" #include "theory/rewriter.h" #include "theory/theory.h" #include "theory/theory_state.h" diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h index 76fcee411..5949441d8 100644 --- a/src/theory/datatypes/proof_checker.h +++ b/src/theory/datatypes/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__DATATYPES__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f9d08dfc2..dc57e4165 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -21,12 +21,12 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/kind.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" +#include "proof/proof_node_manager.h" #include "smt/logic_exception.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" diff --git a/src/theory/fp/fp_expand_defs.h b/src/theory/fp/fp_expand_defs.h index a9edc8b02..8240f1f8e 100644 --- a/src/theory/fp/fp_expand_defs.h +++ b/src/theory/fp/fp_expand_defs.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 8e802f875..b681dad17 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -18,8 +18,8 @@ #ifndef CVC5__THEORY__OUTPUT_CHANNEL_H #define CVC5__THEORY__OUTPUT_CHANNEL_H +#include "proof/trust_node.h" #include "theory/incomplete_id.h" -#include "theory/trust_node.h" #include "util/resource_manager.h" namespace cvc5 { diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index e73323e48..aa7e183bb 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -508,13 +508,13 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) // must use partial substitute here, to avoid substitution into witness std::map<Kind, bool> rkinds; nn = partialSubstitute(t1, vars, subs, rkinds); + nn = Rewriter::rewrite(nn); if (nn != t1) { // If full=false, then we've duplicated a term u in the children of n. // For example, when ITE pulling, we have n is of the form: // ite( C, f( u, t1 ), f( u, t2 ) ) // We must show that at least one copy of u dissappears in this case. - nn = Rewriter::rewrite(nn); if (nn == t2) { new_ret = nn; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 9effdbec7..71f4028ec 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -15,12 +15,12 @@ #include "theory/quantifiers/instantiate.h" -#include "expr/lazy_proof.h" #include "expr/node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "proof/lazy_proof.h" +#include "proof/proof_node_manager.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 9b410dd08..95a396d51 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -22,7 +22,7 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/inference_id.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/quant_util.h" diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h index 618ac8301..23441772e 100644 --- a/src/theory/quantifiers/proof_checker.h +++ b/src/theory/quantifiers/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index cfc4eca2e..ae7f75f34 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -18,8 +18,8 @@ #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#include "proof/trust_node.h" #include "theory/theory_rewriter.h" -#include "theory/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index c9234db2c..fa91b1782 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -17,11 +17,11 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" -#include "expr/proof.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "proof/proof.h" +#include "proof/proof_node_manager.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_registry.h" diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 2a09913a9..c8e6ec7dd 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -24,8 +24,8 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "expr/type_node.h" -#include "theory/eager_proof_generator.h" -#include "theory/trust_node.h" +#include "proof/eager_proof_generator.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 6bfedb0a2..c74146c9c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -15,8 +15,8 @@ #include "theory/quantifiers/theory_quantifiers.h" -#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" +#include "proof/proof_node_manager.h" #include "theory/quantifiers/quantifiers_macros.h" #include "theory/quantifiers/quantifiers_modules.h" #include "theory/quantifiers/quantifiers_rewriter.h" diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 1094d5920..eeb2f166d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -15,8 +15,8 @@ #include "theory/rewriter.h" -#include "expr/term_conversion_proof_generator.h" #include "options/theory_options.h" +#include "proof/conv_proof_generator.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index 87f25341e..f88596ffe 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -22,7 +22,7 @@ #include <vector> #include "context/cdhashmap.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" #include "theory/sets/inference_manager.h" #include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 40f6080e5..b684ff56f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -22,10 +22,10 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" +#include "proof/trust_node.h" #include "theory/ee_setup_info.h" #include "theory/theory_id.h" -#include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" #include "util/statistics_stats.h" diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h index 2cb1c6738..277daf88c 100644 --- a/src/theory/skolem_lemma.h +++ b/src/theory/skolem_lemma.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__SKOLEM_LEMMA_H #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 8ee29f712..d214babae 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -15,10 +15,10 @@ #include "theory/strings/infer_proof_cons.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/strings_options.h" +#include "proof/proof_node_manager.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" #include "theory/strings/regexp_operation.h" @@ -712,11 +712,11 @@ void InferProofCons::convert(InferenceId infer, } else if (eunf.getKind() == AND) { - // equality is the last conjunct + // equality is the first conjunct std::vector<Node> childrenAE; childrenAE.push_back(eunf); std::vector<Node> argsAE; - argsAE.push_back(nm->mkConst(Rational(eunf.getNumChildren() - 1))); + argsAE.push_back(nm->mkConst(Rational(0))); Node eunfAE = psb.tryStep(PfRule::AND_ELIM, childrenAE, argsAE); Trace("strings-ipc-prefix") << "--- and elim to " << eunfAE << std::endl; diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index af905cbad..bba03dd28 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -21,12 +21,12 @@ #include <vector> #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_rule.h" +#include "proof/proof_checker.h" +#include "proof/proof_rule.h" +#include "proof/theory_proof_step_buffer.h" #include "theory/builtin/proof_checker.h" #include "theory/strings/infer_info.h" #include "theory/strings/sequences_stats.h" -#include "theory/theory_proof_step_buffer.h" #include "theory/uf/proof_equality_engine.h" namespace cvc5 { diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index cf9c64bb1..da44100f9 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -24,7 +24,7 @@ #include "context/cdhashset.h" #include "context/context.h" #include "expr/node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include "theory/ext_theory.h" #include "theory/inference_manager_buffered.h" #include "theory/output_channel.h" diff --git a/src/theory/strings/proof_checker.h b/src/theory/strings/proof_checker.h index d3ede53ec..56afaed84 100644 --- a/src/theory/strings/proof_checker.h +++ b/src/theory/strings/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__STRINGS__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 4b033b7bd..f635cdc39 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -15,8 +15,8 @@ #include "theory/strings/regexp_elim.h" -#include "expr/proof_node_manager.h" #include "options/strings_options.h" +#include "proof/proof_node_manager.h" #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" @@ -88,10 +88,10 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // have a fixed length. // The intuition why this is a "non-aggressive" rewrite is that membership // into fixed length regular expressions are easy to handle. - bool hasFixedLength = true; // the index of _* in re unsigned pivotIndex = 0; bool hasPivotIndex = false; + bool hasFixedLength = true; std::vector<Node> childLengths; std::vector<Node> childLengthsPostPivot; for (unsigned i = 0, size = children.size(); i < size; i++) @@ -105,27 +105,32 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) { hasPivotIndex = true; pivotIndex = i; - // set to zero for the sum below + // zero is used in sum below and is used for concat-fixed-len fl = zero; } else { hasFixedLength = false; - break; } } - childLengths.push_back(fl); - if (hasPivotIndex) + if (!fl.isNull()) { - childLengthsPostPivot.push_back(fl); + childLengths.push_back(fl); + if (hasPivotIndex) + { + childLengthsPostPivot.push_back(fl); + } } } + Node lenSum = childLengths.size() > 1 + ? nm->mkNode(PLUS, childLengths) + : (childLengths.empty() ? zero : childLengths[0]); + // if we have a fixed length if (hasFixedLength) { Assert(re.getNumChildren() == children.size()); - Node sum = nm->mkNode(PLUS, childLengths); std::vector<Node> conc; - conc.push_back(nm->mkNode(hasPivotIndex ? GEQ : EQUAL, lenx, sum)); + conc.push_back(nm->mkNode(hasPivotIndex ? GEQ : EQUAL, lenx, lenSum)); Node currEnd = zero; for (unsigned i = 0, size = childLengths.size(); i < size; i++) { @@ -326,7 +331,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node fit = nm->mkNode(LEQ, nm->mkNode(PLUS, prev_end, cEnd), lenx); conj.push_back(fit); } - Node res = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); + Node res = nm->mkAnd(conj); // process the non-greedy find variables if (!non_greedy_find_vars.empty()) { @@ -342,19 +347,23 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node bvl = nm->mkNode(BOUND_VAR_LIST, non_greedy_find_vars); res = nm->mkNode(EXISTS, bvl, body); } + // must also give a minimum length requirement + res = nm->mkNode(AND, res, nm->mkNode(GEQ, lenx, lenSum)); // Examples of this elimination: // x in (re.++ "A" (re.* _) "B" (re.* _)) ---> // substr(x,0,1)="A" ^ indexof(x,"B",1)!=-1 // x in (re.++ (re.* _) "A" _ _ _ (re.* _) "B" _ _ (re.* _)) ---> // indexof(x,"A",0)!=-1 ^ // indexof( x, "B", indexof( x, "A", 0 ) + 1 + 3 ) != -1 ^ - // indexof( x, "B", indexof( x, "A", 0 ) + 1 + 3 )+1+2 <= len(x) + // indexof( x, "B", indexof( x, "A", 0 ) + 1 + 3 )+1+2 <= len(x) ^ + // len(x) >= 7 // An example of a non-greedy find: // x in re.++( re.*( _ ), "A", _, "B", re.*( _ ) ) ---> - // exists k. 0 <= k < len( x ) ^ + // (exists k. 0 <= k < len( x ) ^ // indexof( x, "A", k ) != -1 ^ - // substr( x, indexof( x, "A", k )+2, 1 ) = "B" + // substr( x, indexof( x, "A", k )+2, 1 ) = "B") ^ + // len(x) >= 3 return returnElim(atom, res, "concat-with-gaps"); } } diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index 5387548de..6187a7137 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -18,8 +18,8 @@ #define CVC5__THEORY__STRINGS__REGEXP_ELIM_H #include "expr/node.h" -#include "theory/eager_proof_generator.h" -#include "theory/trust_node.h" +#include "proof/eager_proof_generator.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index bf4c20f85..96351cda9 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -1017,16 +1017,7 @@ Node RegExpOpr::reduceRegExpPos(Node mem, { std::vector<Node> nvec; std::vector<Node> cc; - // get the (valid) existential for this membership - Node eform = getExistsForRegExpConcatMem(mem); SkolemManager* sm = nm->getSkolemManager(); - // Notice that this rule does not introduce witness terms, instead it - // uses skolems in the conclusion of the proof rule directly. Thus, - // the existential eform does not need to be explicitly justified by a - // proof here, since it is only being used as an intermediate formula in - // this inference. Hence we do not pass a proof generator to mkSkolemize. - sm->mkSkolemize(eform, newSkolems, "rc", "regexp concat skolem"); - Assert(newSkolems.size() == r.getNumChildren()); // Look up skolems for each of the components. If sc has optimizations // enabled, this will return arguments of str.to_re. for (unsigned i = 0, nchild = r.getNumChildren(); i < nchild; ++i) @@ -1034,17 +1025,22 @@ Node RegExpOpr::reduceRegExpPos(Node mem, if (r[i].getKind() == STRING_TO_REGEXP) { // optimization, just take the body - newSkolems[i] = r[i][0]; + newSkolems.push_back(r[i][0]); } else { + Node ivalue = nm->mkConst(Rational(i)); + Node sk = sm->mkSkolemFunction(SkolemFunId::RE_UNFOLD_POS_COMPONENT, + s.getType(), + {mem[0], mem[1], ivalue}); + newSkolems.push_back(sk); nvec.push_back(nm->mkNode(STRING_IN_REGEXP, newSkolems[i], r[i])); } } - // (str.in_re x (re.++ R1 .... Rn)) => - // (and (str.in_re k1 R1) ... (str.in_re kn Rn) (= x (str.++ k1 ... kn))) + // (str.in_re x (re.++ R0 .... Rn)) => + // (and (= x (str.++ k0 ... kn)) (str.in_re k0 R0) ... (str.in_re kn Rn) ) Node lem = s.eqNode(nm->mkNode(STRING_CONCAT, newSkolems)); - nvec.push_back(lem); + nvec.insert(nvec.begin(), lem); conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec); } else if (k == REGEXP_STAR) @@ -1574,50 +1570,6 @@ bool RegExpOpr::regExpIncludes(Node r1, Node r2) return result; } -/** - * Associating formulas with their "exists form", or an existentially - * quantified formula that is equivalent to it. This is currently used - * for regular expression memberships in the method below. - */ -struct ExistsFormAttributeId -{ -}; -typedef expr::Attribute<ExistsFormAttributeId, Node> ExistsFormAttribute; - -Node RegExpOpr::getExistsForRegExpConcatMem(Node mem) -{ - // get or make the exists form of the membership - ExistsFormAttribute efa; - if (mem.hasAttribute(efa)) - { - // already computed - return mem.getAttribute(efa); - } - Assert(mem.getKind() == STRING_IN_REGEXP); - Node x = mem[0]; - Node r = mem[1]; - Assert(r.getKind() == REGEXP_CONCAT); - NodeManager* nm = NodeManager::currentNM(); - TypeNode xtn = x.getType(); - std::vector<Node> vars; - std::vector<Node> mems; - for (const Node& rc : r) - { - Node v = nm->mkBoundVar(xtn); - vars.push_back(v); - mems.push_back(nm->mkNode(STRING_IN_REGEXP, v, rc)); - } - Node sconcat = nm->mkNode(STRING_CONCAT, vars); - Node eq = x.eqNode(sconcat); - mems.insert(mems.begin(), eq); - Node bvl = nm->mkNode(BOUND_VAR_LIST, vars); - Node ebody = nm->mkNode(AND, mems); - Node eform = nm->mkNode(EXISTS, bvl, ebody); - mem.setAttribute(efa, eform); - Trace("regexp-opr") << "Exists form " << mem << " : " << eform << std::endl; - return eform; -} - } // namespace strings } // namespace theory } // namespace cvc5 diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index a20e9a0a9..04b5a999d 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -190,18 +190,6 @@ class RegExpOpr { bool regExpIncludes(Node r1, Node r2); private: - /** - * Given a regular expression membership of the form: - * (str.in_re x (re.++ R1 ... Rn)) - * This returns the valid existentially quantified formula: - * (exists ((x1 String) ... (xn String)) - * (=> (str.in_re x (re.++ R1 ... Rn)) - * (and (= x (str.++ x1 ... xn)) - * (str.in_re x1 R1) ... (str.in_re xn Rn)))) - * Moreover, this formula is cached per regular expression membership via - * an attribute, meaning it is always the same for a given membership mem. - */ - static Node getExistsForRegExpConcatMem(Node mem); /** pointer to the skolem cache used by this class */ SkolemCache* d_sc; }; diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 7c399759b..7d660e019 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -20,8 +20,8 @@ #include "context/cdhashset.h" #include "context/cdlist.h" -#include "expr/proof_node_manager.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node_manager.h" #include "theory/output_channel.h" #include "theory/strings/infer_info.h" #include "theory/strings/sequences_stats.h" diff --git a/src/theory/theory.h b/src/theory/theory.h index 8f69d4cb2..d71348ce3 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -28,12 +28,12 @@ #include "context/context.h" #include "expr/node.h" #include "options/theory_options.h" +#include "proof/trust_node.h" #include "theory/assertion.h" #include "theory/care_graph.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" #include "theory/theory_id.h" -#include "theory/trust_node.h" #include "theory/valuation.h" #include "util/statistics_stats.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index abbca451a..676351dd5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -20,15 +20,15 @@ #include "base/map_util.h" #include "decision/decision_engine.h" #include "expr/attribute.h" -#include "expr/lazy_proof.h" #include "expr/node_builder.h" #include "expr/node_visitor.h" -#include "expr/proof_checker.h" -#include "expr/proof_ensure_closed.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" +#include "proof/lazy_proof.h" +#include "proof/proof_checker.h" +#include "proof/proof_ensure_closed.h" #include "prop/prop_engine.h" #include "smt/dump.h" #include "smt/env.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6887959ed..ffcaf392f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -25,6 +25,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "options/theory_options.h" +#include "proof/trust_node.h" #include "theory/atom_requests.h" #include "theory/engine_output_channel.h" #include "theory/interrupted.h" @@ -32,7 +33,6 @@ #include "theory/sort_inference.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" -#include "theory/trust_node.h" #include "theory/trust_substitutions.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index 609d7ae8a..f10716bd9 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -17,7 +17,7 @@ #include <sstream> -#include "expr/proof_node.h" +#include "proof/proof_node.h" using namespace cvc5::kind; diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index 48969aa21..ab0f616fe 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -22,10 +22,10 @@ #include "context/cdhashmap.h" #include "context/context.h" -#include "expr/lazy_proof.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "theory/trust_node.h" +#include "proof/lazy_proof.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 2cb7d9d30..06806f8d4 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -22,10 +22,10 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" +#include "proof/trust_node.h" #include "theory/inference_id.h" #include "theory/output_channel.h" -#include "theory/trust_node.h" #include "util/statistics_stats.h" namespace cvc5 { diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 65bd160fc..230c23424 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -15,8 +15,8 @@ #include "theory/theory_preprocessor.h" -#include "expr/lazy_proof.h" #include "expr/skolem_manager.h" +#include "proof/lazy_proof.h" #include "smt/logic_exception.h" #include "theory/logic_info.h" #include "theory/rewriter.h" diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 58dd763e0..6015f2b07 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -22,13 +22,13 @@ #include "context/cdhashmap.h" #include "context/context.h" -#include "expr/lazy_proof.h" #include "expr/node.h" -#include "expr/tconv_seq_proof_generator.h" -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" +#include "proof/conv_seq_proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/trust_node.h" #include "smt/term_formula_removal.h" #include "theory/skolem_lemma.h" -#include "theory/trust_node.h" namespace cvc5 { diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index 031e32db4..eca1e4e56 100644 --- a/src/theory/theory_rewriter.h +++ b/src/theory/theory_rewriter.h @@ -21,7 +21,7 @@ #define CVC5__THEORY__THEORY_REWRITER_H #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 136992fbe..2a6997d1d 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -21,14 +21,14 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" #include "context/context.h" -#include "expr/lazy_proof.h" -#include "expr/proof_node_manager.h" -#include "expr/proof_set.h" -#include "expr/term_conversion_proof_generator.h" -#include "theory/eager_proof_generator.h" +#include "proof/conv_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/proof_node_manager.h" +#include "proof/proof_set.h" +#include "proof/theory_proof_step_buffer.h" +#include "proof/trust_node.h" #include "theory/substitutions.h" -#include "theory/theory_proof_step_buffer.h" -#include "theory/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index c63f8b51d..fbed7ffb5 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -16,9 +16,9 @@ #include "theory/uf/eq_proof.h" #include "base/configuration.h" -#include "expr/proof.h" -#include "expr/proof_checker.h" #include "options/uf_options.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h index 55f7db3ba..caeda828e 100644 --- a/src/theory/uf/proof_checker.h +++ b/src/theory/uf/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__UF__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index ab36cd9df..b4522d9df 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -15,9 +15,9 @@ #include "theory/uf/proof_equality_engine.h" -#include "expr/lazy_proof_chain.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/lazy_proof_chain.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "theory/rewriter.h" #include "theory/uf/eq_proof.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 4ca13d93f..0c093d4b2 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -22,10 +22,10 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" -#include "expr/buffered_proof_generator.h" -#include "expr/lazy_proof.h" #include "expr/node.h" -#include "theory/eager_proof_generator.h" +#include "proof/buffered_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/lazy_proof.h" namespace cvc5 { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9cf47bab3..1afb8cc31 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -21,11 +21,11 @@ #include <sstream> #include "expr/node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "proof/proof_node_manager.h" #include "smt/logic_exception.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" |