Towards disentangling Options / NodeManager / SmtEngine.
This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.
The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.
The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.
It also removes the solver in src/theory/idl, which cannot be enabled after this commit.
cvc4_option(ENABLE_DUMPING "Enable dumping")
cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output")
cvc4_option(ENABLE_PROOFS "Enable proof support")
-cvc4_option(ENABLE_REPLAY "Enable the replay feature")
cvc4_option(ENABLE_STATISTICS "Enable statistics")
cvc4_option(ENABLE_TRACING "Enable tracing")
cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing")
add_definitions(-DCVC4_PROOF)
endif()
-if(ENABLE_REPLAY)
- add_definitions(-DCVC4_REPLAY)
-endif()
-
if(ENABLE_TRACING)
add_definitions(-DCVC4_TRACING)
endif()
print_config("Dumping :" ENABLE_DUMPING)
print_config("Muzzle :" ENABLE_MUZZLE)
print_config("Proofs :" ENABLE_PROOFS)
-print_config("Replay :" ENABLE_REPLAY)
print_config("Statistics :" ENABLE_STATISTICS)
print_config("Tracing :" ENABLE_TRACING)
message("")
cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF)
# enable_statistics=no
cvc4_set_option(ENABLE_STATISTICS OFF)
-# enable_replay=no
-cvc4_set_option(ENABLE_REPLAY OFF)
# enable_assertions=no
cvc4_set_option(ENABLE_ASSERTIONS OFF)
# enable_proof=no
cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON)
# enable_statistics=yes
cvc4_set_option(ENABLE_STATISTICS ON)
-# enable_replay=yes
-cvc4_set_option(ENABLE_REPLAY ON)
# enable_assertions=yes
cvc4_set_option(ENABLE_ASSERTIONS ON)
# enable_proof=yes
cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF)
# enable_statistics=yes
cvc4_set_option(ENABLE_STATISTICS ON)
-# enable_replay=no
-cvc4_set_option(ENABLE_REPLAY OFF)
# enable_assertions=no
cvc4_set_option(ENABLE_ASSERTIONS OFF)
# enable_proof=yes
cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON)
# enable_statistics=yes
cvc4_set_option(ENABLE_STATISTICS ON)
-# enable_replay=yes
-cvc4_set_option(ENABLE_REPLAY ON)
# enable_assertions=yes
cvc4_set_option(ENABLE_ASSERTIONS ON)
# enable_proof=yes
--valgrind Valgrind instrumentation
--debug-context-mm use the debug context memory manager
--statistics include statistics
- --replay turn on the replay feature
--assertions turn on assertions
--tracing include tracing code
--dumping include dumping code
muzzle=default
optimized=default
proofs=default
-replay=default
shared=default
static_binary=default
statistics=default
--proofs) proofs=ON;;
--no-proofs) proofs=OFF;;
- --replay) replay=ON;;
- --no-replay) replay=OFF;;
-
--static) shared=OFF; static_binary=ON;;
--no-static) shared=ON;;
&& cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized"
[ $proofs != default ] \
&& cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs"
-[ $replay != default ] \
- && cmake_opts="$cmake_opts -DENABLE_REPLAY=$replay"
[ $shared != default ] \
&& cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
[ $static_binary != default ] \
theory/fp/theory_fp_rewriter.h
theory/fp/theory_fp_type_rules.h
theory/fp/type_enumerator.h
- theory/idl/idl_assertion.cpp
- theory/idl/idl_assertion.h
- theory/idl/idl_assertion_db.cpp
- theory/idl/idl_assertion_db.h
- theory/idl/idl_model.cpp
- theory/idl/idl_model.h
- theory/idl/theory_idl.cpp
- theory/idl/theory_idl.h
theory/interrupted.h
theory/logic_info.cpp
theory/logic_info.h
${PROJECT_SOURCE_DIR}/src/theory/sep/kinds
${PROJECT_SOURCE_DIR}/src/theory/sets/kinds
${PROJECT_SOURCE_DIR}/src/theory/strings/kinds
- ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds
- ${PROJECT_SOURCE_DIR}/src/theory/idl/kinds)
+ ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds)
#-----------------------------------------------------------------------------#
# Add subdirectories
expr/datatype.h
expr/emptyset.h
expr/expr_iomanip.h
- expr/expr_stream.h
expr/record.h
expr/symbol_table.h
expr/type.h
return IS_STATISTICS_BUILD;
}
-bool Configuration::isReplayBuild() {
- return IS_REPLAY_BUILD;
-}
-
bool Configuration::isTracingBuild() {
return IS_TRACING_BUILD;
}
static bool isStatisticsBuild();
- static bool isReplayBuild();
-
static bool isTracingBuild();
static bool isDumpingBuild();
# define IS_STATISTICS_BUILD false
#endif /* CVC4_STATISTICS_ON */
-#ifdef CVC4_REPLAY
-# define IS_REPLAY_BUILD true
-#else /* CVC4_REPLAY */
-# define IS_REPLAY_BUILD false
-#endif /* CVC4_REPLAY */
-
#ifdef CVC4_TRACING
# define IS_TRACING_BUILD true
#else /* CVC4_TRACING */
${CMAKE_CURRENT_BINARY_DIR}/ExprHashFunction.java
${CMAKE_CURRENT_BINARY_DIR}/ExprManager.java
${CMAKE_CURRENT_BINARY_DIR}/ExprManagerMapCollection.java
- ${CMAKE_CURRENT_BINARY_DIR}/ExprStream.java
${CMAKE_CURRENT_BINARY_DIR}/FloatingPoint.java
${CMAKE_CURRENT_BINARY_DIR}/FloatingPointConvertSort.java
${CMAKE_CURRENT_BINARY_DIR}/FloatingPointSize.java
// The remainder of the includes:
%include "expr/expr.i"
%include "expr/expr_manager.i"
-%include "expr/expr_stream.i"
%include "expr/variable_type_map.i"
%include "options/option_exception.i"
%include "options/options.i"
expr_iomanip.cpp
expr_iomanip.h
expr_manager_scope.h
- expr_stream.h
kind_map.h
match_trie.cpp
match_trie.h
+++ /dev/null
-/********************* */
-/*! \file expr_stream.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 A stream interface for expressions
- **
- ** A stream interface for expressions.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__EXPR_STREAM_H
-#define CVC4__EXPR_STREAM_H
-
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-/**
- * A pure-virtual stream interface for expressions. Can be used to
- * communicate streams of expressions between different parts of CVC4.
- */
-class CVC4_PUBLIC ExprStream {
-public:
- /** Virtual destructor; this implementation does nothing. */
- virtual ~ExprStream() {}
-
- /**
- * Get the next expression in the stream (advancing the stream
- * pointer as a side effect.)
- */
- virtual Expr nextExpr() = 0;
-};/* class ExprStream */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__EXPR_STREAM_H */
-
+++ /dev/null
-%{
-#include "expr/expr_stream.h"
-%}
-
-%include "expr/expr_stream.h"
#line 205 "${template}"
-namespace theory {
-
-static inline bool useTheoryValidate(std::string theory) {
-${use_theory_validations}
- return false;
-}
-
-static const char *const useTheoryHelp = "\
-The following options are valid alternate implementations for use with\n\
-the --use-theory option:\n\
-\n\
-${theory_alternate_doc}";
-
-}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
metakind_lbchildren=
metakind_operatorKinds=
-use_theory_validations=
-theory_alternate_doc=
-
seen_theory=false
seen_theory_builtin=false
theory_header="$4"
theory_includes="${theory_includes}#include \"$theory_header\"
"
-
- use_theory_validations="${use_theory_validations}
- if(theory == \"$name\") {
- return true;
- }"
- theory_alternate_doc="$theory_alternate_doc$name - alternate implementation for $theory_id\\n\\
-"
}
function properties {
nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' |
awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
-if [ -z "$theory_alternate_doc" ]; then
- theory_alternate_doc="[none defined]"
-fi
-
text=$(cat "$template")
for var in \
metakind_includes \
metakind_ubchildren \
metakind_lbchildren \
metakind_operatorKinds \
- use_theory_validations \
- theory_alternate_doc \
template \
; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
d_smtEngine(d_solver->getSmtEngine()),
d_options(options),
d_stats("driver"),
- d_result(),
- d_replayStream(nullptr)
+ d_result()
{
}
d_stats.safeFlushInformation(fd);
}
-void CommandExecutor::setReplayStream(ExprStream* replayStream) {
- assert(d_replayStream == NULL);
- d_replayStream = replayStream;
- d_smtEngine->setReplayStream(d_replayStream);
-}
-
bool CommandExecutor::doCommand(Command* cmd)
{
if( d_options.getParseOnly() ) {
Options& d_options;
StatisticsRegistry d_stats;
Result d_result;
- ExprStream* d_replayStream;
public:
CommandExecutor(Options& options);
virtual ~CommandExecutor()
{
- if (d_replayStream != NULL)
- {
- delete d_replayStream;
- }
}
/**
void flushOutputStreams();
- void setReplayStream(ExprStream* replayStream);
-
protected:
/** Executes treating cmd as a singleton */
virtual bool doCommandSingleton(CVC4::Command* cmd);
// Create the command executor to execute the parsed commands
pExecutor = new CommandExecutor(opts);
- std::unique_ptr<Parser> replayParser;
- if (opts.getReplayInputFilename() != "")
- {
- std::string replayFilename = opts.getReplayInputFilename();
- ParserBuilder replayParserBuilder(
- pExecutor->getSolver(), replayFilename, opts);
-
- if( replayFilename == "-") {
- if( inputFromStdin ) {
- throw OptionException("Replay file and input file can't both be stdin.");
- }
- replayParserBuilder.withStreamInput(cin);
- }
- replayParser.reset(replayParserBuilder.build());
- pExecutor->setReplayStream(new Parser::ExprStream(replayParser.get()));
- }
-
int returnValue = 0;
{
// Timer statistic
<< endl << endl;
Message() << Configuration::copyright() << endl;
}
- if(replayParser) {
- // have the replay parser use the declarations input interactively
- replayParser->useDeclarationsFrom(shell.getParser());
- }
while(true) {
try {
vector< vector<Command*> > allCommands;
allCommands.push_back(vector<Command*>());
std::unique_ptr<Parser> parser(parserBuilder.build());
- if(replayParser) {
- // have the replay parser use the file's declarations
- replayParser->useDeclarationsFrom(parser.get());
- }
int needReset = 0;
// true if one of the commands was interrupted
bool interrupted = false;
}
std::unique_ptr<Parser> parser(parserBuilder.build());
- if(replayParser) {
- // have the replay parser use the file's declarations
- replayParser->useDeclarationsFrom(parser.get());
- }
bool interrupted = false;
while (status)
{
decision_options.toml
expr_options.toml
fp_options.toml
- idl_options.toml
main_options.toml
parser_options.toml
printer_options.toml
+++ /dev/null
-id = "IDL"
-name = "Idl"
-header = "options/idl_options.h"
-
-[[option]]
- name = "idlRewriteEq"
- category = "regular"
- long = "idl-rewrite-equalities"
- type = "bool"
- default = "false"
- help = "enable rewriting equalities into two inequalities in IDL solver (default is disabled)"
/** Listeners for options::tlimit-per. */
ListenerCollection d_rlimitPerListeners;
- /** Listeners for options::useTheoryList. */
- ListenerCollection d_useTheoryListListeners;
-
/** Listeners for options::defaultExprDepth. */
ListenerCollection d_setDefaultExprDepthListeners;
/** Listeners for options::diagnosticChannelName. */
ListenerCollection d_setDiagnosticChannelListeners;
- /** Listeners for options::replayFilename. */
- ListenerCollection d_setReplayFilenameListeners;
-
-
static ListenerCollection::Registration* registerAndNotify(
ListenerCollection& collection, Listener* listener, bool notify);
std::ostream* getOut();
std::ostream* getOutConst() const; // TODO: Remove this.
std::string getBinaryName() const;
- std::string getReplayInputFilename() const;
unsigned getParseStep() const;
// TODO: Document these.
ListenerCollection::Registration* registerRlimitPerListener(
Listener* listener, bool notifyIfSet);
- /**
- * Registers a listener for options::useTheoryList being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerUseTheoryListListener(
- Listener* listener, bool notifyIfSet);
-
-
/**
* Registers a listener for options::defaultExprDepth being set.
*
ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener(
Listener* listener, bool notifyIfSet);
- /**
- * Registers a listener for options::replayLogFilename being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerSetReplayLogFilename(
- Listener* listener, bool notifyIfSet);
-
/** Sends a std::flush to getErr(). */
void flushErr();
}
}
-// theory/options_handlers.h
-std::string OptionsHandler::handleUseTheoryList(std::string option, std::string optarg) {
- std::string currentList = options::useTheoryList();
- if(currentList.empty()){
- return optarg;
- } else {
- return currentList +','+ optarg;
- }
-}
-
-void OptionsHandler::notifyUseTheoryList(std::string option) {
- d_options->d_useTheoryListListeners.notify();
-}
-
// printer/options_handlers.h
const std::string OptionsHandler::s_instFormatHelp = "\
Inst format modes currently supported by the --inst-format option:\n\
d_options->d_setDiagnosticChannelListeners.notify();
}
-
-std::string OptionsHandler::checkReplayFilename(std::string option, std::string optarg) {
-#ifdef CVC4_REPLAY
- if(optarg == "") {
- throw OptionException (std::string("Bad file name for --replay"));
- } else {
- return optarg;
- }
-#else /* CVC4_REPLAY */
- throw OptionException("The replay feature was disabled in this build of CVC4.");
-#endif /* CVC4_REPLAY */
-}
-
-void OptionsHandler::notifySetReplayLogFilename(std::string option) {
- d_options->d_setReplayFilenameListeners.notify();
-}
-
void OptionsHandler::statsEnabledBuild(std::string option, bool value)
{
#ifndef CVC4_STATISTICS_ON
print_config_cond("debug code", Configuration::isDebugBuild());
print_config_cond("statistics", Configuration::isStatisticsBuild());
- print_config_cond("replay", Configuration::isReplayBuild());
print_config_cond("tracing", Configuration::isTracingBuild());
print_config_cond("dumping", Configuration::isDumpingBuild());
print_config_cond("muzzled", Configuration::isMuzzledBuild());
void setBitblastAig(std::string option, bool arg);
- // theory/options_handlers.h
- void notifyUseTheoryList(std::string option);
- std::string handleUseTheoryList(std::string option, std::string optarg);
-
// printer/options_handlers.h
InstFormatMode stringToInstFormatMode(std::string option, std::string optarg);
void notifyDumpToFile(std::string option);
void notifySetRegularOutputChannel(std::string option);
void notifySetDiagnosticOutputChannel(std::string option);
- std::string checkReplayFilename(std::string option, std::string optarg);
- void notifySetReplayLogFilename(std::string option);
void statsEnabledBuild(std::string option, bool value);
return (*this)[options::binary_name];
}
-std::string Options::getReplayInputFilename() const{
- return (*this)[options::replayInputFilename];
-}
-
unsigned Options::getParseStep() const{
return (*this)[options::parseStep];
}
return registerAndNotify(d_rlimitPerListeners, listener, notify);
}
-ListenerCollection::Registration* Options::registerUseTheoryListListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::useTheoryList);
- return registerAndNotify(d_useTheoryListListeners, listener, notify);
-}
-
ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
Listener* listener, bool notifyIfSet)
{
return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify);
}
-ListenerCollection::Registration*
-Options::registerSetReplayLogFilename(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::replayLogFilename);
- return registerAndNotify(d_setReplayFilenameListeners, listener, notify);
-}
-
${custom_handlers}$
read_only = true
help = "amount of resources spent for each sat conflict (bitvectors)"
-# --replay is currently broken; don't document it for 1.0
-[[option]]
- name = "replayInputFilename"
- category = "undocumented"
- long = "replay=FILE"
- type = "std::string"
- handler = "checkReplayFilename"
- read_only = true
- help = "replay decisions from file"
-
-# --replay is currently broken; don't document it for 1.0
-[[option]]
- name = "replayLogFilename"
- category = "undocumented"
- long = "replay-log=FILE"
- type = "std::string"
- handler = "checkReplayFilename"
- notifies = ["notifySetReplayLogFilename", "notifyBeforeSearch"]
- read_only = true
- help = "replay decisions from file"
-
[[option]]
name = "forceNoLimitCpuWhileDump"
category = "regular"
name = "term"
help = "Type variables as uninterpreted, type constants by theory, equalities by the parametric theory."
-[[option]]
- name = "useTheoryList"
- smt_name = "use-theory"
- category = "regular"
- long = "use-theory=NAME"
- type = "std::string"
- handler = "handleUseTheoryList"
- notifies = ["notifyUseTheoryList"]
- read_only = true
- help = "use alternate theory implementation NAME (--use-theory=help for a list). This option may be repeated or a comma separated list."
-
[[option]]
name = "assignFunctionValues"
category = "regular"
* declared in the outer context. What follows isn't quite right,
* though, since type aliases and function definitions should be
* retained in the set of current declarations. */
- { /*symtab = PARSER_STATE->getSymbolTable();
- PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ }
formula[f] ( COMMA formula[f2] )? RPAREN
{
PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release");
#include "api/cvc4cpp.h"
#include "expr/expr.h"
-#include "expr/expr_stream.h"
#include "expr/kind.h"
#include "expr/symbol_table.h"
#include "parser/input.h"
d_globalDeclarations = flag;
}
- /**
- * Set the current symbol table used by this parser.
- * From now on, this parser will perform its definitions and
- * lookups in the declaration scope of the "parser" argument
- * (but doesn't re-delegate if the other parser's declaration scope
- * changes later). A NULL argument restores this parser's
- * "primordial" declaration scope assigned at its creation. Calling
- * p->useDeclarationsFrom(p) is a no-op.
- *
- * This feature is useful when e.g. reading out-of-band expression data:
- * 1. Parsing --replay log files produced with --replay-log.
- * 2. Perhaps a multi-query benchmark file is being single-stepped
- * with intervening queries on stdin that must reference the same
- * declaration scope(s).
- *
- * However, the feature must be used carefully. Pushes and pops
- * should be performed with the correct current declaration scope.
- * Care must be taken to match up declaration scopes, of course;
- * If variables in the deferred-to parser go out of scope, the
- * secondary parser will give errors that they are undeclared.
- * Also, an outer-scope variable shadowed by an inner-scope one of
- * the same name may be temporarily inaccessible.
- *
- * In short, caveat emptor.
- */
- inline void useDeclarationsFrom(Parser* parser) {
- if(parser == NULL) {
- d_symtab = &d_symtabAllocated;
- } else {
- d_symtab = parser->d_symtab;
- }
- }
-
- inline void useDeclarationsFrom(SymbolTable* symtab) {
- d_symtab = symtab;
- }
-
inline SymbolTable* getSymbolTable() const {
return d_symtab;
}
-
- /**
- * An expression stream interface for a parser. This stream simply
- * pulls expressions from the given Parser object.
- *
- * Here, the ExprStream base class allows a Parser (from the parser
- * library) and core components of CVC4 (in the core library) to
- * communicate without polluting the public interface or having them
- * reach into private (undocumented) interfaces.
- */
- class ExprStream : public CVC4::ExprStream {
- Parser* d_parser;
- public:
- ExprStream(Parser* parser) : d_parser(parser) {}
- ~ExprStream() { delete d_parser; }
- Expr nextExpr() override { return d_parser->nextExpression().getExpr(); }
- };/* class Parser::ExprStream */
//------------------------ operator overloading
/** is this function overloaded? */
{
Lit nextLit;
-#ifdef CVC4_REPLAY
-
- nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextReplayDecision());
-
- if (nextLit != lit_Undef) {
- return nextLit;
- }
-#endif /* CVC4_REPLAY */
-
// Theory requests
nextLit =
MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest());
check_type = CHECK_FINAL;
continue;
}
-
-#ifdef CVC4_REPLAY
- d_proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
-#endif /* CVC4_REPLAY */
}
// Increase decision level and enqueue 'next'
using namespace std;
using namespace CVC4::context;
-
-#ifdef CVC4_REPLAY
-# define CVC4_USE_REPLAY true
-#else /* CVC4_REPLAY */
-# define CVC4_USE_REPLAY false
-#endif /* CVC4_REPLAY */
-
namespace CVC4 {
namespace prop {
PropEngine::PropEngine(TheoryEngine* te,
Context* satContext,
- UserContext* userContext,
- std::ostream* replayLog,
- ExprStream* replayStream)
+ UserContext* userContext)
: d_inCheckSat(false),
d_theoryEngine(te),
d_context(satContext),
d_cnfStream = new CVC4::prop::TseitinCnfStream(
d_satSolver, d_registrar, userContext, true);
- d_theoryProxy = new TheoryProxy(this,
- d_theoryEngine,
- d_decisionEngine.get(),
- d_context,
- d_cnfStream,
- replayLog,
- replayStream);
+ d_theoryProxy = new TheoryProxy(
+ this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
d_satSolver->initialize(d_context, d_theoryProxy);
d_decisionEngine->setSatSolver(d_satSolver);
#include <sys/time.h>
#include "base/modal_exception.h"
-#include "expr/expr_stream.h"
#include "expr/node.h"
#include "options/options.h"
#include "preprocessing/assertion_pipeline.h"
*/
PropEngine(TheoryEngine*,
context::Context* satContext,
- context::UserContext* userContext,
- std::ostream* replayLog,
- ExprStream* replayStream);
+ context::UserContext* userContext);
/**
* Destructor.
#include "context/context.h"
#include "decision/decision_engine.h"
-#include "expr/expr_stream.h"
#include "options/decision_options.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
TheoryEngine* theoryEngine,
DecisionEngine* decisionEngine,
context::Context* context,
- CnfStream* cnfStream,
- std::ostream* replayLog,
- ExprStream* replayStream)
+ CnfStream* cnfStream)
: d_propEngine(propEngine),
d_cnfStream(cnfStream),
d_decisionEngine(decisionEngine),
d_theoryEngine(theoryEngine),
- d_replayLog(replayLog),
- d_replayStream(replayStream),
- d_queue(context),
- d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0)
+ d_queue(context)
{
- smtStatisticsRegistry()->registerStat(&d_replayedDecisions);
}
TheoryProxy::~TheoryProxy() {
/* nothing to do for now */
- smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions);
}
void TheoryProxy::variableNotify(SatVariable var) {
d_theoryEngine->notifyRestart();
}
-SatLiteral TheoryProxy::getNextReplayDecision() {
-#ifdef CVC4_REPLAY
- if(d_replayStream != NULL) {
- Expr e = d_replayStream->nextExpr();
- if(!e.isNull()) { // we get null node when out of decisions to replay
- // convert & return
- ++d_replayedDecisions;
- return d_cnfStream->getLiteral(e);
- }
- }
-#endif /* CVC4_REPLAY */
- return undefSatLiteral;
-}
-
-void TheoryProxy::logDecision(SatLiteral lit) {
-#ifdef CVC4_REPLAY
- if(d_replayLog != NULL) {
- Assert(lit != undefSatLiteral) << "logging an `undef' decision ?!";
- (*d_replayLog) << d_cnfStream->getNode(lit) << std::endl;
- }
-#endif /* CVC4_REPLAY */
-}
-
void TheoryProxy::spendResource(ResourceManager::Resource r)
{
d_theoryEngine->spendResource(r);
#include <unordered_set>
#include "context/cdqueue.h"
-#include "expr/expr_stream.h"
#include "expr/node.h"
#include "prop/sat_solver.h"
#include "theory/theory.h"
TheoryEngine* theoryEngine,
DecisionEngine* decisionEngine,
context::Context* context,
- CnfStream* cnfStream,
- std::ostream* replayLog,
- ExprStream* replayStream);
+ CnfStream* cnfStream);
~TheoryProxy();
void notifyRestart();
- SatLiteral getNextReplayDecision();
-
- void logDecision(SatLiteral lit);
-
void spendResource(ResourceManager::Resource r);
bool isDecisionEngineDone();
/** The theory engine we are using. */
TheoryEngine* d_theoryEngine;
- /** Stream on which to log replay events. */
- std::ostream* d_replayLog;
-
- /** Stream for replaying decisions. */
- ExprStream* d_replayStream;
-
/** Queue of asserted facts */
context::CDQueue<TNode> d_queue;
*/
std::unordered_set<Node, NodeHashFunction> d_shared;
- /**
- * Statistic: the number of replayed decisions (via --replay).
- */
- IntStat d_replayedDecisions;
-
}; /* class SatSolver */
}/* CVC4::prop namespace */
opener->addSpecialCase("stderr", &std::cerr);
}
-
-ManagedReplayLogOstream::ManagedReplayLogOstream() : d_replayLog(NULL) {}
-ManagedReplayLogOstream::~ManagedReplayLogOstream(){
- if(d_replayLog != NULL) {
- (*d_replayLog) << std::flush;
- }
-}
-
-std::string ManagedReplayLogOstream::defaultSource() const {
- return options::replayLogFilename();
-}
-
-void ManagedReplayLogOstream::initialize(std::ostream* outStream) {
- if(outStream != NULL){
- *outStream << language::SetLanguage(options::outputLanguage())
- << expr::ExprSetDepth(-1);
- }
- /* Do this regardless of managing the memory. */
- d_replayLog = outStream;
-}
-
-/** Adds special cases to an ostreamopener. */
-void ManagedReplayLogOstream::addSpecialCases(OstreamOpener* opener) const {
- opener->addSpecialCase("-", &std::cout);
-}
-
-
}/* CVC4 namespace */
void addSpecialCases(OstreamOpener* opener) const override;
};/* class ManagedRegularOutputChannel */
-/** This controls the memory associated with replay-log. */
-class ManagedReplayLogOstream : public ManagedOstream {
- public:
- ManagedReplayLogOstream();
- ~ManagedReplayLogOstream();
-
- std::ostream* getReplayLog() const { return d_replayLog; }
- const char* getName() const override { return "replay-log"; }
- std::string defaultSource() const override;
-
- protected:
- /** Initializes an output stream. Not necessarily managed. */
- void initialize(std::ostream* outStream) override;
-
- /** Adds special cases to an ostreamopener. */
- void addSpecialCases(OstreamOpener* opener) const override;
-
- private:
- std::ostream* d_replayLog;
-};/* class ManagedRegularOutputChannel */
-
}/* CVC4 namespace */
#endif /* CVC4__MANAGED_OSTREAMS_H */
SmtEngine* d_smt;
}; /* class BeforeSearchListener */
-class UseTheoryListListener : public Listener {
- public:
- UseTheoryListListener(TheoryEngine* theoryEngine)
- : d_theoryEngine(theoryEngine)
- {}
-
- void notify() override
- {
- std::stringstream commaList(options::useTheoryList());
- std::string token;
-
- Debug("UseTheoryListListener") << "UseTheoryListListener::notify() "
- << options::useTheoryList() << std::endl;
-
- while(std::getline(commaList, token, ',')){
- if(token == "help") {
- puts(theory::useTheoryHelp);
- exit(1);
- }
- if(theory::useTheoryValidate(token)) {
- d_theoryEngine->enableTheoryAlternative(token);
- } else {
- throw OptionException(
- std::string("unknown option for --use-theory : `") + token +
- "'. Try --use-theory=help.");
- }
- }
- }
-
- private:
- TheoryEngine* d_theoryEngine;
-}; /* class UseTheoryListListener */
-
-
class SetDefaultExprDepthListener : public Listener {
public:
void notify() override
/** Manager for the memory of --dump-to. */
ManagedDumpOStream d_managedDumpChannel;
- /** Manager for --replay-log. */
- ManagedReplayLogOstream d_managedReplayLog;
-
/**
* This list contains:
* softResourceOut
* hardResourceOut
* beforeSearchListener
- * UseTheoryListListener
*
* This needs to be deleted before both NodeManager's Options,
* SmtEngine, d_resourceManager, and TheoryEngine.
d_managedRegularChannel(),
d_managedDiagnosticChannel(),
d_managedDumpChannel(),
- d_managedReplayLog(),
d_listenerRegistrations(new ListenerRegistrationList()),
d_propagator(true, true),
d_assertions(),
d_listenerRegistrations->add(
nodeManagerOptions.registerDumpToFileNameListener(
new SetToDefaultSourceListener(&d_managedDumpChannel), true));
- d_listenerRegistrations->add(
- nodeManagerOptions.registerSetReplayLogFilename(
- new SetToDefaultSourceListener(&d_managedReplayLog), true));
}
catch (OptionException& e)
{
return retval;
}
- void addUseTheoryListListener(TheoryEngine* theoryEngine){
- Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
- d_listenerRegistrations->add(
- nodeManagerOptions.registerUseTheoryListListener(
- new UseTheoryListListener(theoryEngine), true));
- }
-
- std::ostream* getReplayLog() const {
- return d_managedReplayLog.getReplayLog();
- }
-
//------------------------------- expression names
// implements setExpressionName, as described in smt_engine.h
void setExpressionName(Expr e, std::string name) {
d_status(),
d_expectedStatus(),
d_smtMode(SMT_MODE_START),
- d_replayStream(nullptr),
d_private(nullptr),
d_statisticsRegistry(nullptr),
d_stats(nullptr)
#endif
}
- d_private->addUseTheoryListListener(getTheoryEngine());
-
// set the random seed
Random::getRandom().setSeed(options::seed());
* are unregistered by the obsolete PropEngine object before registered
* again by the new PropEngine object */
d_propEngine.reset(nullptr);
- d_propEngine.reset(new PropEngine(getTheoryEngine(),
- getContext(),
- getUserContext(),
- d_private->getReplayLog(),
- d_replayStream));
+ d_propEngine.reset(
+ new PropEngine(getTheoryEngine(), getContext(), getUserContext()));
Trace("smt-debug") << "Setting up theory engine..." << std::endl;
d_theoryEngine->setPropEngine(getPropEngine());
* statistics are unregistered by the obsolete PropEngine object before
* registered again by the new PropEngine object */
d_propEngine.reset(nullptr);
- d_propEngine.reset(new PropEngine(getTheoryEngine(),
- getContext(),
- getUserContext(),
- d_private->getReplayLog(),
- d_replayStream));
+ d_propEngine.reset(
+ new PropEngine(getTheoryEngine(), getContext(), getUserContext()));
d_theoryEngine->setPropEngine(getPropEngine());
}
return SExpr::parseAtom(nodeManagerOptions.getOption(key));
}
-void SmtEngine::setReplayStream(ExprStream* replayStream) {
- AlwaysAssert(!d_fullyInited)
- << "Cannot set replay stream once fully initialized";
- d_replayStream = replayStream;
-}
-
bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
return d_private->getExpressionName(e, name);
}
#include "context/cdlist_forward.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
-#include "expr/expr_stream.h"
#include "options/options.h"
#include "proof/unsat_core.h"
#include "smt/logic_exception.h"
*/
void beforeSearch();
- /**
- * Expermintal feature: Sets the sequence of decisions.
- * This currently requires very fine grained knowledge about literal
- * translation.
- */
- void setReplayStream(ExprStream* exprStream);
-
/**
* Get expression name.
*
*/
std::map<std::string, Integer> d_commandVerbosity;
- /** ReplayStream for the solver. */
- ExprStream* d_replayStream;
-
/**
* A private utility class to SmtEngine.
*/
+++ /dev/null
-/********************* */
-/*! \file idl_assertion.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/idl/idl_assertion.h"
-
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-IDLAssertion::IDLAssertion()
-: d_op(kind::LAST_KIND)
-{}
-
-IDLAssertion::IDLAssertion(TNode node) {
- bool ok = parse(node, 1, false);
- if (!ok) {
- d_x = d_y = TNode::null();
- } else {
- if (d_op == kind::GT) {
- // Turn GT into LT x - y > c is the same as y - x < -c
- std::swap(d_x, d_y);
- d_c = -d_c;
- d_op = kind::LT;
- }
- if (d_op == kind::GEQ) {
- // Turn GT into LT x - y >= c is the same as y - x <= -c
- std::swap(d_x, d_y);
- d_c = -d_c;
- d_op = kind::LEQ;
- }
- if (d_op == kind::LT) {
- // Turn strict into non-strict x - y < c is the same as x - y <= c-1
- d_c = d_c - 1;
- d_op = kind::LEQ;
- }
- }
- d_original = node;
-}
-
-IDLAssertion::IDLAssertion(const IDLAssertion& other)
-: d_x(other.d_x)
-, d_y(other.d_y)
-, d_op(other.d_op)
-, d_c(other.d_c)
-, d_original(other.d_original)
-{}
-
-bool IDLAssertion::propagate(IDLModel& model) const {
- Debug("theory::idl::model") << model << std::endl;
- Assert(ok());
- // Should be d_x - d_y <= d_c, or d_x - d_c <= d_y
- Integer x_value = model.getValue(d_x);
- Integer y_value = model.getValue(d_y);
- if (x_value - y_value > d_c) {
- model.setValue(d_y, x_value - d_c, IDLReason(d_x, d_original));
- Debug("theory::idl::model") << model << std::endl;
- return true;
- } else {
- return false;
- }
-}
-
-void IDLAssertion::toStream(std::ostream& out) const {
- out << "IDL[" << d_x << " - " << d_y << " " << d_op << " " << d_c << "]";
-}
-
-/** Negates the given arithmetic kind */
-static Kind negateOp(Kind op) {
- switch (op) {
- case kind::LT:
- // not (a < b) = (a >= b)
- return kind::GEQ;
- case kind::LEQ:
- // not (a <= b) = (a > b)
- return kind::GT;
- case kind::GT:
- // not (a > b) = (a <= b)
- return kind::LEQ;
- case kind::GEQ:
- // not (a >= b) = (a < b)
- return kind::LT;
- case kind::EQUAL:
- // not (a = b) = (a != b)
- return kind::DISTINCT;
- case kind::DISTINCT:
- // not (a != b) = (a = b)
- return kind::EQUAL;
- default:
- Unreachable();
- break;
- }
- return kind::LAST_KIND;
-}
-
-bool IDLAssertion::parse(TNode node, int c, bool negated) {
-
- // Only unit coefficients allowed
- if (c != 1 && c != -1) {
- return false;
- }
-
- // Assume we're ok
- bool ok = true;
-
- // The kind of the node
- switch(node.getKind()) {
-
- case kind::NOT:
- // We parse the negation
- ok = parse(node[0], c, true);
- // Setup the kind
- if (ok) {
- d_op = negateOp(d_op);
- }
- break;
-
- case kind::EQUAL:
- case kind::LT:
- case kind::LEQ:
- case kind::GT:
- case kind::GEQ: {
- // All relation operators are parsed on both sides
- d_op = node.getKind();
- ok = parse(node[0], c, negated);
- if (ok) {
- ok = parse(node[1],-c, negated);
- }
- break;
- }
-
- case kind::CONST_RATIONAL: {
- // Constants
- Rational m = node.getConst<Rational>();
- if (m.isIntegral()) {
- d_c += m.getNumerator() * (-c);
- } else {
- ok = false;
- }
- break;
- }
- case kind::MULT: {
- // Only unit multiplication of variables
- if (node.getNumChildren() == 2 && node[0].isConst()) {
- Rational a = node[0].getConst<Rational>();
- if (a == 1 || a == -1) {
- ok = parse(node[1], c * a.sgn(), negated);
- } else {
- ok = false;
- }
- } else {
- ok = false;
- }
- break;
- }
-
- case kind::PLUS: {
- for(unsigned i = 0; i < node.getNumChildren(); ++i) {
- ok = parse(node[i], c, negated);
- if(!ok) {
- break;
- }
- }
- break;
- }
-
- case kind::MINUS: {
- ok = parse(node[0], c, negated);
- if (ok) {
- ok = parse(node[1], -c, negated);
- }
- break;
- }
-
- case kind::UMINUS: {
- ok = parse(node[0], -c, negated);
- break;
- }
-
- default: {
- if (c > 0) {
- if (d_x.isNull()) {
- d_x = node;
- } else {
- ok = false;
- }
- } else {
- if (d_y.isNull()) {
- d_y = node;
- } else {
- ok = false;
- }
- }
- break;
- }
- } // End case
-
- // Difference logic OK
- return ok;
-}
+++ /dev/null
-/********************* */
-/*! \file idl_assertion.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#pragma once
-
-#include "theory/idl/idl_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-/**
- * An internal representation of the IDL assertions. Each IDL assertions is
- * of the form (x - y op c) where op is one of (<=, =, !=). IDL assertion
- * can be constructed from an expression.
- */
-class IDLAssertion {
-
- /** The positive variable */
- TNode d_x;
- /** The negative variable */
- TNode d_y;
- /** The relation */
- Kind d_op;
- /** The RHS constant */
- Integer d_c;
-
- /** Original assertion we got this one from */
- TNode d_original;
-
- /** Parses the given node into an assertion, and return true if OK. */
- bool parse(TNode node, int c = 1, bool negated = false);
-
-public:
-
- /** Null assertion */
- IDLAssertion();
- /** Create the assertion from given node */
- IDLAssertion(TNode node);
- /** Copy constructor */
- IDLAssertion(const IDLAssertion& other);
-
- TNode getX() const { return d_x; }
- TNode getY() const { return d_y; }
- Kind getOp() const { return d_op;}
- Integer getC() const { return d_c; }
-
- /**
- * Propagate the constraint using the model. For example, if the constraint
- * is of the form x - y <= -1, and the value of x in the model is 0, then
- *
- * (x - y <= -1) and (x = 0) implies y >= x + 1 = 1
- *
- * If the value of y is less then 1, is is set to 1 and true is returned. If
- * the value of y is 1 or more, than false is return.
- *
- * @return true if value of y was updated
- */
- bool propagate(IDLModel& model) const;
-
- /** Is this constraint proper */
- bool ok() const {
- return !d_x.isNull() || !d_y.isNull();
- }
-
- /** Output to the stream */
- void toStream(std::ostream& out) const;
-};
-
-inline std::ostream& operator << (std::ostream& out, const IDLAssertion& assertion) {
- assertion.toStream(out);
- return out;
-}
-
-}
-}
-}
+++ /dev/null
-/********************* */
-/*! \file idl_assertion_db.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/idl/idl_assertion_db.h"
-
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-IDLAssertionDB::IDLAssertionDB(context::Context* c)
-: d_assertions(c)
-, d_variableLists(c)
-{}
-
-void IDLAssertionDB::add(const IDLAssertion& assertion, TNode var) {
- // Is there a list for the variable already?
- unsigned previous = -1;
- var_to_unsigned_map::iterator find = d_variableLists.find(var);
- if (find != d_variableLists.end()) {
- previous = (*find).second;
- }
- // Add to the DB
- d_variableLists[var] = d_assertions.size();
- d_assertions.push_back(IDLAssertionListElement(assertion, previous));
-}
-
-IDLAssertionDB::iterator::iterator(IDLAssertionDB& db, TNode var)
-: d_db(db)
-, d_current(-1)
-{
- var_to_unsigned_map::const_iterator find = d_db.d_variableLists.find(var);
- if (find != d_db.d_variableLists.end()) {
- d_current = (*find).second;
- }
-}
-
-void IDLAssertionDB::iterator::next() {
- if (d_current != (unsigned)(-1)) {
- d_current = d_db.d_assertions[d_current].d_previous;
- }
-}
-
-IDLAssertion IDLAssertionDB::iterator::get() const {
- return d_db.d_assertions[d_current].d_assertion;
-}
+++ /dev/null
-/********************* */
-/*! \file idl_assertion_db.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#pragma once
-
-#include "theory/idl/idl_assertion.h"
-#include "context/cdlist.h"
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-/**
- * Context-dependent database assertions, organized by variable. Each variable
- * can be associated a list of IDL assertions. The list of assertions can
- * be iterated over using the provided iterator class.
- */
-class IDLAssertionDB {
-
- /** Elements of the assertion lists */
- struct IDLAssertionListElement {
- /** The assertion itself */
- IDLAssertion d_assertion;
- /** The index of the previous element (-1 for null) */
- unsigned d_previous;
-
- IDLAssertionListElement(const IDLAssertion& assertion, unsigned previous)
- : d_assertion(assertion), d_previous(previous)
- {}
- };
-
- /** All assertions in a context dependent stack */
- context::CDList<IDLAssertionListElement> d_assertions;
-
- typedef context::CDHashMap<TNode, unsigned, TNodeHashFunction> var_to_unsigned_map;
-
- /** Map from variables to the first element of their list */
- var_to_unsigned_map d_variableLists;
-
-public:
-
- /** Create a new assertion database */
- IDLAssertionDB(context::Context* c);
-
- /** Add a new assertion, attach to the list of the given variable */
- void add(const IDLAssertion& assertion, TNode var);
-
- /** Iteration over the constraints of a variable */
- class iterator {
- /** The database */
- const IDLAssertionDB& d_db;
- /** Index of the current constraint */
- unsigned d_current;
- public:
- /** Construct the iterator for the variable */
- iterator(IDLAssertionDB& db, TNode var);
- /** Is this iterator done */
- bool done() const { return d_current == (unsigned)(-1); }
- /** Next element */
- void next();
- /** Get the assertion */
- IDLAssertion get() const;
- };
-};
-
-}
-}
-}
-
-
-
-
+++ /dev/null
-/********************* */
-/*! \file idl_model.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/idl/idl_model.h"
-
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-IDLModel::IDLModel(context::Context* context)
- : d_model(context), d_reason(context)
-{
-}
-
-Integer IDLModel::getValue(TNode var) const
-{
- model_value_map::const_iterator find = d_model.find(var);
- if (find != d_model.end())
- {
- return (*find).second;
- }
- else
- {
- return 0;
- }
-}
-
-void IDLModel::setValue(TNode var, Integer value, IDLReason reason)
-{
- Assert(!reason.d_constraint.isNull());
- d_model[var] = value;
- d_reason[var] = reason;
-}
-
-void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons)
-{
- TNode current = var;
- do
- {
- Debug("theory::idl::model") << "processing: " << var << std::endl;
- Assert(d_reason.find(current) != d_reason.end());
- IDLReason reason = d_reason[current];
- Debug("theory::idl::model")
- << "adding reason: " << reason.d_constraint << std::endl;
- reasons.push_back(reason.d_constraint);
- current = reason.d_x;
- } while (current != var);
-}
-
-void IDLModel::toStream(std::ostream& out) const
-{
- model_value_map::const_iterator it = d_model.begin();
- model_value_map::const_iterator it_end = d_model.end();
- out << "Model[" << std::endl;
- for (; it != it_end; ++it)
- {
- out << (*it).first << " -> " << (*it).second << std::endl;
- }
- out << "]";
-}
+++ /dev/null
-/********************* */
-/*! \file idl_model.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#pragma once
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-/**
- * A reason for a value of a variable in the model is a constraint that implies
- * this value by means of the value of another variable. For example, if the
- * value of x is 0, then the variable x and the constraint (y > 0) are a reason
- * for the y taking the value 1.
- */
-struct IDLReason
-{
- /** The variable of the reason */
- TNode d_x;
- /** The constraint of the reason */
- TNode d_constraint;
-
- IDLReason(TNode x, TNode constraint) : d_x(x), d_constraint(constraint) {}
- IDLReason() {}
-};
-
-/**
- * A model maps variables to integer values and backs them up with reasons.
- * Default values (if not set with setValue) for all variables are 0.
- */
-class IDLModel
-{
- typedef context::CDHashMap<TNode, Integer, TNodeHashFunction> model_value_map;
- typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction>
- model_reason_map;
-
- /** Values assigned to individual variables */
- model_value_map d_model;
-
- /** Reasons constraining the individual variables */
- model_reason_map d_reason;
-
- public:
- IDLModel(context::Context* context);
-
- /** Get the model value of the variable */
- Integer getValue(TNode var) const;
-
- /** Set the value of the variable */
- void setValue(TNode var, Integer value, IDLReason reason);
-
- /** Get the cycle of reasons behind the variable var */
- void getReasonCycle(TNode var, std::vector<TNode>& reasons);
-
- /** Output to the given stream */
- void toStream(std::ostream& out) const;
-};
-
-inline std::ostream& operator<<(std::ostream& out, const IDLModel& model)
-{
- model.toStream(out);
- return out;
-}
-
-} // namespace idl
-} // namespace theory
-} // namespace CVC4
+++ /dev/null
-# kinds -*- sh -*-
-#
-# For documentation on this file format, please refer to
-# src/theory/builtin/kinds.
-#
-
-alternate THEORY_ARITH "idl" ::CVC4::theory::idl::TheoryIdl "theory/idl/theory_idl.h"
-
+++ /dev/null
-/********************* */
-/*! \file theory_idl.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/idl/theory_idl.h"
-
-#include <set>
-#include <queue>
-
-#include "options/idl_options.h"
-#include "theory/rewriter.h"
-
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u,
- OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo)
- : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
- , d_model(c)
- , d_assertionsDB(c)
-{}
-
-Node TheoryIdl::ppRewrite(TNode atom) {
- if (atom.getKind() == kind::EQUAL && options::idlRewriteEq()) {
- // If the option is turned on, each equality into two inequalities. This in
- // effect removes equalities, and theorefore dis-equalities too.
- Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
- Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
- Node rewritten = Rewriter::rewrite(leq.andNode(geq));
- return rewritten;
- } else {
- return atom;
- }
-}
-
-void TheoryIdl::check(Effort level) {
- if (done() && !fullEffort(level)) {
- return;
- }
-
- TimerStat::CodeTimer checkTimer(d_checkTime);
-
- while(!done()) {
-
- // Get the next assertion
- Assertion assertion = get();
- Debug("theory::idl") << "TheoryIdl::check(): processing "
- << assertion.d_assertion << std::endl;
-
- // Convert the assertion into the internal representation
- IDLAssertion idlAssertion(assertion.d_assertion);
- Debug("theory::idl") << "TheoryIdl::check(): got " << idlAssertion << std::endl;
-
- if (idlAssertion.ok()) {
- if (idlAssertion.getOp() == kind::DISTINCT) {
- // We don't handle dis-equalities
- d_out->setIncomplete();
- } else {
- // Process the convex assertions immediately
- bool ok = processAssertion(idlAssertion);
- if (!ok) {
- // In conflict, we're done
- return;
- }
- }
- } else {
- // Not an IDL assertion, set incomplete
- d_out->setIncomplete();
- }
- }
-
-}
-
-bool TheoryIdl::processAssertion(const IDLAssertion& assertion) {
-
- Debug("theory::idl") << "TheoryIdl::processAssertion(" << assertion << ")" << std::endl;
-
- // Add the constraint (x - y op c) to the list assertions of x
- d_assertionsDB.add(assertion, assertion.getX());
-
- // Update the model, if forced by the assertion
- bool y_updated = assertion.propagate(d_model);
-
- // If the value of y was updated, we might need to update further
- if (y_updated) {
-
- std::queue<TNode> queue; // Queue of variables to consider
- std::set<TNode> inQueue; // Current elements of the queue
-
- // Add the first updated variable to the queue
- queue.push(assertion.getY());
- inQueue.insert(assertion.getY());
-
- while (!queue.empty()) {
- // Pop a new variable x off the queue
- TNode x = queue.front();
- queue.pop();
- inQueue.erase(x);
-
- // Go through the constraint (x - y op c), and update values of y
- IDLAssertionDB::iterator it(d_assertionsDB, x);
- while (!it.done()) {
- // Get the assertion and update y
- IDLAssertion x_y_assertion = it.get();
- y_updated = x_y_assertion.propagate(d_model);
- // If updated add to the queue
- if (y_updated) {
- // If the variable that we updated is the same as the first
- // variable that we updated, it's a cycle of updates => conflict
- if (x_y_assertion.getY() == assertion.getX()) {
- std::vector<TNode> reasons;
- d_model.getReasonCycle(x_y_assertion.getY(), reasons);
- // Construct the reason of the conflict
- Node conflict = NodeManager::currentNM()->mkNode(kind::AND, reasons);
- d_out->conflict(conflict);
- return false;
- } else {
- // No cycle, just a model update, so we add to the queue
- TNode y = x_y_assertion.getY();
- if (inQueue.count(y) == 0) {
- queue.push(y);
- inQueue.insert(x_y_assertion.getY());
- }
- }
- }
- // Go to the next constraint
- it.next();
- }
- }
- }
-
- // Everything fine, no conflict
- return true;
-}
-
-} /* namepsace CVC4::theory::idl */
-} /* namepsace CVC4::theory */
-} /* namepsace CVC4 */
+++ /dev/null
-/********************* */
-/*! \file theory_idl.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Dejan Jovanovic, Mathias Preiner, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#pragma once
-
-#include "cvc4_private.h"
-
-#include "theory/theory.h"
-#include "theory/idl/idl_model.h"
-#include "theory/idl/idl_assertion_db.h"
-
-namespace CVC4 {
-namespace theory {
-namespace idl {
-
-/**
- * Handles integer difference logic (IDL) constraints.
- */
-class TheoryIdl : public Theory {
-
- /** The current model */
- IDLModel d_model;
-
- /** The asserted constraints, organized by variable */
- IDLAssertionDB d_assertionsDB;
-
- /** Process a new assertion, returns false if in conflict */
- bool processAssertion(const IDLAssertion& assertion);
-
-public:
-
- /** Theory constructor. */
- TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo);
-
- /** Pre-processing of input atoms */
- Node ppRewrite(TNode atom) override;
-
- /** Check the assertions for satisfiability */
- void check(Effort effort) override;
-
- /** Identity string */
- std::string identify() const override { return "THEORY_IDL"; }
-
-};/* class TheoryIdl */
-
-}/* CVC4::theory::idl namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
theory_header="$4"
theory_includes="${theory_includes}#include \"$theory_header\"
"
-
- eval "alternate_for_$1=\"\${alternate_for_$1}
- if(engine->useTheoryAlternative(\\\"$2\\\")) {
- engine->addTheory< $3 >($1);
- return;
- }\""
}
function rewriter {
d_factsAsserted(context, false),
d_preRegistrationVisitor(this, context),
d_sharedTermsVisitor(d_sharedTerms),
- d_theoryAlternatives(),
d_attr_handle(),
d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
{
d_resourceManager->spendResource(r);
}
-void TheoryEngine::enableTheoryAlternative(const std::string& name){
- Debug("TheoryEngine::enableTheoryAlternative")
- << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl;
-
- d_theoryAlternatives.insert(name);
-}
-
-bool TheoryEngine::useTheoryAlternative(const std::string& name) {
- return d_theoryAlternatives.find(name) != d_theoryAlternatives.end();
-}
-
-
TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
conflicts(getStatsPrefix(theory) + "::conflicts", 0),
propagations(getStatsPrefix(theory) + "::propagations", 0),
/** Prints the assertions to the debug stream */
void printAssertions(const char* tag);
- /** Theory alternative is in use. */
- bool useTheoryAlternative(const std::string& name);
-
- /** Enables using a theory alternative by name. */
- void enableTheoryAlternative(const std::string& name);
-
private:
- std::set< std::string > d_theoryAlternatives;
std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
projects / cvc5.git / commitdiff