diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-12 13:18:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-12 13:18:13 -0500 |
commit | f4f11801394afa718a5125e4386704a72e74ca48 (patch) | |
tree | 05ebc80af205de90000942de8cfb58a906fcc890 /src/theory/decision_strategy.cpp | |
parent | 700a21a55d277d7bb4e475849e98aab58d91dba5 (diff) |
Initial infrastructure for theory decision manager (#2447)
Diffstat (limited to 'src/theory/decision_strategy.cpp')
-rw-r--r-- | src/theory/decision_strategy.cpp | 145 |
1 files changed, 145 insertions, 0 deletions
diff --git a/src/theory/decision_strategy.cpp b/src/theory/decision_strategy.cpp new file mode 100644 index 000000000..fcd11f6ba --- /dev/null +++ b/src/theory/decision_strategy.cpp @@ -0,0 +1,145 @@ +/********************* */ +/*! \file decision_strategy.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief Implementation of base classes for decision strategies used by theory + ** solvers for use in the DecisionManager of TheoryEngine. + **/ + +#include "theory/decision_strategy.h" + +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext, + Valuation valuation) + : d_valuation(valuation), + d_has_curr_literal(false, satContext), + d_curr_literal(0, satContext) +{ +} + +void DecisionStrategyFmf::initialize() { d_literals.clear(); } + +Node DecisionStrategyFmf::getNextDecisionRequest() +{ + Trace("dec-strategy-debug") + << "Get next decision request " << identify() << "..." << std::endl; + if (d_has_curr_literal.get()) + { + Trace("dec-strategy-debug") << "...already has decision" << std::endl; + return Node::null(); + } + bool success; + unsigned curr_lit = d_curr_literal.get(); + do + { + success = true; + // get the current literal + Node lit = getLiteral(curr_lit); + Trace("dec-strategy-debug") + << "...check literal #" << curr_lit << " : " << lit << std::endl; + // if out of literals, we are done in the current SAT context + if (!lit.isNull()) + { + bool value; + if (!d_valuation.hasSatValue(lit, value)) + { + Trace("dec-strategy-debug") << "...not assigned, return." << std::endl; + // if it has not been decided, return it + return lit; + } + else if (!value) + { + Trace("dec-strategy-debug") + << "...assigned false, increment." << std::endl; + // asserted false, the current literal is incremented + curr_lit = d_curr_literal.get() + 1; + d_curr_literal.set(curr_lit); + // repeat + success = false; + } + else + { + Trace("dec-strategy-debug") << "...already assigned true." << std::endl; + } + } + else + { + Trace("dec-strategy-debug") << "...exhausted literals." << std::endl; + } + } while (!success); + // the current literal has been decided with the right polarity, we are done + d_has_curr_literal = true; + return Node::null(); +} + +bool DecisionStrategyFmf::getAssertedLiteralIndex(unsigned& i) const +{ + if (d_has_curr_literal.get()) + { + i = d_curr_literal.get(); + return true; + } + return false; +} + +Node DecisionStrategyFmf::getAssertedLiteral() +{ + if (d_has_curr_literal.get()) + { + Assert(d_curr_literal.get() < d_literals.size()); + return getLiteral(d_curr_literal.get()); + } + return Node::null(); +} + +Node DecisionStrategyFmf::getLiteral(unsigned n) +{ + // allocate until the index is valid + while (n >= d_literals.size()) + { + Node lit = mkLiteral(d_literals.size()); + if (!lit.isNull()) + { + lit = Rewriter::rewrite(lit); + lit = d_valuation.ensureLiteral(lit); + } + d_literals.push_back(lit); + } + return d_literals[n]; +} + +DecisionStrategySingleton::DecisionStrategySingleton( + const char* name, + Node lit, + context::Context* satContext, + Valuation valuation) + : DecisionStrategyFmf(satContext, valuation), d_name(name), d_literal(lit) +{ +} + +Node DecisionStrategySingleton::mkLiteral(unsigned n) +{ + if (n == 0) + { + return d_literal; + } + return Node::null(); +} + +Node DecisionStrategySingleton::getSingleLiteral() { return d_literal; } + +} // namespace theory +} // namespace CVC4 |