diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-17 17:20:37 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-17 17:20:37 +0000 |
commit | 7742c4211f765c2ba2637a211265c20789b861ee (patch) | |
tree | 05622a9df5dc2c900608b8e2ac5611d70e3208c6 /src/decision/decision_strategy.h | |
parent | ccd77233892ace44fd4852999e66534d1c2283ea (diff) |
A dummy decision engine. Expected performance impact: none.
Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.
Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin
Diffstat (limited to 'src/decision/decision_strategy.h')
-rw-r--r-- | src/decision/decision_strategy.h | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h new file mode 100644 index 000000000..abcbbaace --- /dev/null +++ b/src/decision/decision_strategy.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file decision_strategy.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Decision stategy + ** + ** Decision strategy + **/ + +#ifndef __CVC4__DECISION__DECISION_STRATEGY_H +#define __CVC4__DECISION__DECISION_STRATEGY_H + +#include "prop/sat_solver_types.h" + +namespace CVC4 { + +class DecisionEngine; + +namespace decision { + +class DecisionStrategy { +protected: + DecisionEngine* d_decisionEngine; +public: + DecisionStrategy(DecisionEngine* de) : + d_decisionEngine(de) { + } + + virtual ~DecisionStrategy() { } + + virtual prop::SatLiteral getNext() = 0; + + virtual bool needSimplifiedPreITEAssertions() { return false; } + + virtual void notifyAssertionsAvailable() { return; } +}; + +}/* decision namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__DECISION__DECISION_STRATEGY_H */ |