From fafde0249bec12df91370119f35fc020ec81c935 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Apr 2021 21:34:35 -0500 Subject: [PATCH] Add basic utilities for new implementation of justification heuristic (#6333) This sets up the core utilities for the new implementation of justification heuristic --- src/CMakeLists.txt | 6 +++ src/decision/justify_info.cpp | 52 ++++++++++++++++++++ src/decision/justify_info.h | 60 +++++++++++++++++++++++ src/decision/justify_stack.cpp | 90 ++++++++++++++++++++++++++++++++++ src/decision/justify_stack.h | 81 ++++++++++++++++++++++++++++++ src/decision/justify_stats.cpp | 42 ++++++++++++++++ src/decision/justify_stats.h | 48 ++++++++++++++++++ 7 files changed, 379 insertions(+) create mode 100644 src/decision/justify_info.cpp create mode 100644 src/decision/justify_info.h create mode 100644 src/decision/justify_stack.cpp create mode 100644 src/decision/justify_stack.h create mode 100644 src/decision/justify_stats.cpp create mode 100644 src/decision/justify_stats.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9e340a31c..82c556559 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -25,6 +25,12 @@ libcvc4_add_sources( 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 diff --git a/src/decision/justify_info.cpp b/src/decision/justify_info.cpp new file mode 100644 index 000000000..8ed3718a3 --- /dev/null +++ b/src/decision/justify_info.cpp @@ -0,0 +1,52 @@ +/****************************************************************************** + * 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 diff --git a/src/decision/justify_info.h b/src/decision/justify_info.h new file mode 100644 index 000000000..bf8c882b3 --- /dev/null +++ b/src/decision/justify_info.h @@ -0,0 +1,60 @@ +/****************************************************************************** + * 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; + +/** + * 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 d_node; + /** Desired value */ + context::CDO d_desiredVal; + /** The child index we are considering */ + context::CDO d_childIndex; +}; + +} +} // namespace cvc5 + +#endif /* CVC5__DECISION__JUSTIFY_INFO_H */ diff --git a/src/decision/justify_stack.cpp b/src/decision/justify_stack.cpp new file mode 100644 index 000000000..53350e2f6 --- /dev/null +++ b/src/decision/justify_stack.cpp @@ -0,0 +1,90 @@ +/****************************************************************************** + * 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(d_context)); + } + return d_stack[i].get(); +} + +} +} // namespace cvc5 diff --git a/src/decision/justify_stack.h b/src/decision/justify_stack.h new file mode 100644 index 000000000..9a5815a0c --- /dev/null +++ b/src/decision/justify_stack.h @@ -0,0 +1,81 @@ +/****************************************************************************** + * 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 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 > d_stack; + /** Current number of entries in the stack that are valid */ + context::CDO d_stackSizeValid; +}; + +} +} // namespace cvc5 + +#endif /* CVC5__DECISION__JUSTIFY_INFO_H */ diff --git a/src/decision/justify_stats.cpp b/src/decision/justify_stats.cpp new file mode 100644 index 000000000..23bcfab11 --- /dev/null +++ b/src/decision/justify_stats.cpp @@ -0,0 +1,42 @@ +/****************************************************************************** + * 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 diff --git a/src/decision/justify_stats.h b/src/decision/justify_stats.h new file mode 100644 index 000000000..6e53a83df --- /dev/null +++ b/src/decision/justify_stats.h @@ -0,0 +1,48 @@ +/****************************************************************************** + * 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 */ -- 2.30.2