This sets up the core utilities for the new implementation of justification heuristic
decision/decision_strategy.h
decision/justification_heuristic.cpp
decision/justification_heuristic.h
+ decision/justify_info.cpp
+ decision/justify_info.h
+ decision/justify_stack.cpp
+ decision/justify_stack.h
+ decision/justify_stats.cpp
+ decision/justify_stats.h
lib/clock_gettime.c
lib/clock_gettime.h
lib/ffs.c
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Justification info.
+ */
+
+#include "decision/justify_info.h"
+
+namespace cvc5 {
+namespace decision {
+
+JustifyInfo::JustifyInfo(context::Context* c)
+ : d_node(c), d_desiredVal(c, prop::SAT_VALUE_UNKNOWN), d_childIndex(c, 0)
+{
+}
+
+JustifyInfo::~JustifyInfo() {}
+
+JustifyNode JustifyInfo::getNode() const
+{
+ return JustifyNode(d_node.get(), d_desiredVal.get());
+}
+
+size_t JustifyInfo::getNextChildIndex()
+{
+ size_t i = d_childIndex.get();
+ d_childIndex = d_childIndex + 1;
+ return i;
+}
+void JustifyInfo::revertChildIndex()
+{
+ Assert(d_childIndex.get() > 0);
+ d_childIndex = d_childIndex - 1;
+}
+void JustifyInfo::set(TNode n, prop::SatValue desiredVal)
+{
+ d_node = n;
+ d_desiredVal = desiredVal;
+ d_childIndex = 0;
+}
+
+}
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Justification info.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__DECISION__JUSTIFY_INFO_H
+#define CVC5__DECISION__JUSTIFY_INFO_H
+
+#include "context/cdo.h"
+#include "expr/node.h"
+#include "prop/sat_solver_types.h"
+
+namespace cvc5 {
+namespace decision {
+
+/** A pair indicating a node and its desired value */
+using JustifyNode = std::pair<TNode, prop::SatValue>;
+
+/**
+ * Information concerning a single formula in the justification strategy.
+ */
+class JustifyInfo
+{
+ public:
+ JustifyInfo(context::Context* c);
+ ~JustifyInfo();
+ /** set */
+ void set(TNode n, prop::SatValue desiredVal);
+ /** get node */
+ JustifyNode getNode() const;
+ /** get next child index, and increment */
+ size_t getNextChildIndex();
+ /** revert child index */
+ void revertChildIndex();
+
+ private:
+ /** The node we are considering */
+ context::CDO<TNode> d_node;
+ /** Desired value */
+ context::CDO<prop::SatValue> d_desiredVal;
+ /** The child index we are considering */
+ context::CDO<size_t> d_childIndex;
+};
+
+}
+} // namespace cvc5
+
+#endif /* CVC5__DECISION__JUSTIFY_INFO_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Justification stack.
+ */
+
+#include "decision/justify_stack.h"
+
+namespace cvc5 {
+namespace decision {
+
+JustifyStack::JustifyStack(context::Context* c)
+ : d_context(c), d_current(c), d_stack(c), d_stackSizeValid(c, 0)
+{
+}
+JustifyStack::~JustifyStack() {}
+
+void JustifyStack::reset(TNode curr)
+{
+ d_current = curr;
+ d_stackSizeValid = 0;
+ pushToStack(curr, prop::SAT_VALUE_TRUE);
+}
+void JustifyStack::clear()
+{
+ d_current = TNode::null();
+ d_stackSizeValid = 0;
+}
+
+size_t JustifyStack::size() const { return d_stackSizeValid.get(); }
+
+TNode JustifyStack::getCurrentAssertion() const { return d_current.get(); }
+bool JustifyStack::hasCurrentAssertion() const
+{
+ return !d_current.get().isNull();
+}
+JustifyInfo* JustifyStack::getCurrent()
+{
+ if (d_stackSizeValid.get() == 0)
+ {
+ return nullptr;
+ }
+ Assert(d_stack.size() >= d_stackSizeValid.get());
+ return d_stack[d_stackSizeValid.get() - 1].get();
+}
+
+void JustifyStack::pushToStack(TNode n, prop::SatValue desiredVal)
+{
+ if (Trace.isOn("jh-stack"))
+ {
+ for (size_t i = 0, ssize = d_stackSizeValid.get(); i < ssize; i++)
+ {
+ Trace("jh-stack") << " ";
+ }
+ Trace("jh-stack") << "- " << n << " " << desiredVal << std::endl;
+ }
+ // note that n is possibly negated here
+ JustifyInfo* ji = getOrAllocJustifyInfo(d_stackSizeValid.get());
+ ji->set(n, desiredVal);
+ d_stackSizeValid = d_stackSizeValid + 1;
+}
+
+void JustifyStack::popStack()
+{
+ Assert(d_stackSizeValid.get() > 0);
+ d_stackSizeValid = d_stackSizeValid - 1;
+}
+
+JustifyInfo* JustifyStack::getOrAllocJustifyInfo(size_t i)
+{
+ // don't request stack beyond the bound
+ Assert(i <= d_stack.size());
+ if (i == d_stack.size())
+ {
+ d_stack.push_back(std::make_shared<JustifyInfo>(d_context));
+ }
+ return d_stack[i].get();
+}
+
+}
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Justification stack.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__DECISION__JUSTIFY_STACK_H
+#define CVC5__DECISION__JUSTIFY_STACK_H
+
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "decision/justify_info.h"
+#include "expr/node.h"
+
+namespace cvc5 {
+namespace decision {
+
+/**
+ * A justify stack, which tracks the progress in justifying a formula. It
+ * maintains a stack of justification infos in a SAT-context dependent
+ * manner.
+ */
+class JustifyStack
+{
+ public:
+ JustifyStack(context::Context* c);
+ ~JustifyStack();
+ /** reset the stack */
+ void reset(TNode curr);
+ /** clear */
+ void clear();
+ /** size */
+ size_t size() const;
+ /** Get the current assertion */
+ TNode getCurrentAssertion() const;
+ /** Has current assertion */
+ bool hasCurrentAssertion() const;
+ /** Get current justify info */
+ JustifyInfo* getCurrent();
+ /** Push to stack */
+ void pushToStack(TNode n, prop::SatValue desiredVal);
+ /** Pop from stack */
+ void popStack();
+
+ private:
+ /**
+ * Get or allocate justify info at position i. This does not impact
+ * d_stackSizeValid.
+ */
+ JustifyInfo* getOrAllocJustifyInfo(size_t i);
+ /** The context */
+ context::Context* d_context;
+ /** The current assertion we are trying to satisfy */
+ context::CDO<TNode> d_current;
+ /**
+ * Stack of justify info, valid up to index d_stackSizeValid-1. Notice the
+ * size of this list may be larger than the current size we are using in
+ * cases where we considered an assertion requiring a larger stack size
+ * than the current one. This is because we do not erase elements from
+ * CDList in a context-dependent manner.
+ */
+ context::CDList<std::shared_ptr<JustifyInfo> > d_stack;
+ /** Current number of entries in the stack that are valid */
+ context::CDO<size_t> d_stackSizeValid;
+};
+
+}
+} // namespace cvc5
+
+#endif /* CVC5__DECISION__JUSTIFY_INFO_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Justification stats.
+ */
+
+#include "decision/justify_stats.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace cvc5 {
+namespace decision {
+
+JustifyStatistics::JustifyStatistics()
+ : d_numStatusNoDecision(smtStatisticsRegistry().registerInt(
+ "JustifyStrategy::StatusNoDecision", 0)),
+ d_numStatusDecision(smtStatisticsRegistry().registerInt(
+ "JustifyStrategy::StatusDecision", 0)),
+ d_numStatusBacktrack(smtStatisticsRegistry().registerInt(
+ "JustifyStrategy::StatusBacktrack", 0)),
+ d_maxStackSize(smtStatisticsRegistry().registerInt(
+ "JustifyStrategy::MaxStackSize", 0)),
+ d_maxAssertionsSize(smtStatisticsRegistry().registerInt(
+ "JustifyStrategy::MaxAssertionsSize", 0)),
+ d_maxSkolemDefsSize(smtStatisticsRegistry().registerInt(
+ "JustifyStrategy::MaxSkolemDefsSize", 0))
+{
+}
+
+JustifyStatistics::~JustifyStatistics() {}
+
+}
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Justification stats.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__DECISION__JUSTIFY_STATS_H
+#define CVC5__DECISION__JUSTIFY_STATS_H
+
+#include "util/statistics_registry.h"
+
+namespace cvc5 {
+namespace decision {
+
+class JustifyStatistics
+{
+ public:
+ JustifyStatistics();
+ ~JustifyStatistics();
+ /** Number of times we considered an assertion not leading to a decision */
+ IntStat d_numStatusNoDecision;
+ /** Number of times we considered an assertion that led to a decision */
+ IntStat d_numStatusDecision;
+ /** Number of times we considered an assertion that led to backtracking */
+ IntStat d_numStatusBacktrack;
+ /** Maximum stack size we considered */
+ IntStat d_maxStackSize;
+ /** Maximum assertion size we considered */
+ IntStat d_maxAssertionsSize;
+ /** Maximum skolem definition size we considered */
+ IntStat d_maxSkolemDefsSize;
+};
+
+}
+} // namespace cvc5
+
+#endif /* CVC5__DECISION__JUSTIFY_STATS_H */
projects / cvc5.git / commitdiff