diff options
author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/theory/bv/bv_quick_check.h | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/theory/bv/bv_quick_check.h')
-rw-r--r-- | src/theory/bv/bv_quick_check.h | 179 |
1 files changed, 179 insertions, 0 deletions
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h new file mode 100644 index 000000000..c09994c06 --- /dev/null +++ b/src/theory/bv/bv_quick_check.h @@ -0,0 +1,179 @@ +/********************* */ +/*! \file bv_quick_check.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sandboxed sat solver for bv quickchecks. + ** + ** Sandboxed sat solver for bv quickchecks. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BV_QUICK_CHECK_H +#define __CVC4__BV_QUICK_CHECK_H + +#include <vector> +#include <ext/hash_map> + +#include "expr/node.h" +#include "context/cdo.h" +#include "prop/sat_solver_types.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { + +class TheoryModel; + +namespace bv { + + + +typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + +class TLazyBitblaster; +class TheoryBV; + +class BVQuickCheck { + context::Context* d_ctx; + TLazyBitblaster* d_bitblaster; + Node d_conflict; + context::CDO<bool> d_inConflict; + void setConflict(); + +public: + BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv); + ~BVQuickCheck(); + bool inConflict(); + Node getConflict() { return d_conflict; } + /** + * Checks the satisfiability for a given set of assumptions. + * + * @param assumptions literals assumed true + * @param budget max number of conflicts + * + * @return + */ + prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget); + /** + * Checks the satisfiability of given assertions. + * + * @param budget max number of conflicts + * + * @return + */ + prop::SatValue checkSat(unsigned long budget); + + /** + * Convert to CNF and assert the given literal. + * + * @param assumption bv literal + * + * @return false if a conflict has been found via bcp. + */ + bool addAssertion(TNode assumption); + + void push(); + void pop(); + void popToZero(); + /** + * Deletes the SAT solver and CNF stream, but maintains the + * bit-blasting term cache. + * + */ + void clearSolver(); + + /** + * Computes the size of the circuit required to bit-blast + * atom, by not recounting the nodes in seen. + * + * @param node + * @param seen + * + * @return + */ + uint64_t computeAtomWeight(TNode atom, NodeSet& seen); + void collectModelInfo(theory::TheoryModel* model, bool fullModel); + + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator; + vars_iterator beginVars(); + vars_iterator endVars(); + + Node getVarValue(TNode var); + +}; + + +class QuickXPlain { + struct Statistics { + TimerStat d_xplainTime; + IntStat d_numSolved; + IntStat d_numUnknown; + IntStat d_numUnknownWasUnsat; + IntStat d_numConflictsMinimized; + IntStat d_finalPeriod; + AverageStat d_avgMinimizationRatio; + Statistics(const std::string&); + ~Statistics(); + }; + BVQuickCheck* d_solver; + unsigned long d_budget; + + // crazy heuristic variables + unsigned d_numCalled; // number of times called + double d_minRatioSum; // sum of minimization ratio for computing average min ratio + unsigned d_numConflicts; // number of conflicts (including when minimization not applied) + unsigned d_period; // after how many conflicts to try minimizing again + + double d_thresh; // if minimization ratio is less, increase period + double d_hardThresh; // decrease period if minimization ratio is greater than this + + + Statistics d_statistics; + /** + * Uses solve with assumptions unsat core feature to + * further minimize a conflict. The minimized conflict + * will be between low and the returned value in conflict. + * + * @param low + * @param high + * @param conflict + * + * @return + */ + unsigned selectUnsatCore(unsigned low, unsigned high, + std::vector<TNode>& conflict); + /** + * Internal conflict minimization, attempts to minimize + * literals in conflict between low and high and adds the + * result in new_conflict. + * + * @param low + * @param high + * @param conflict + * @param new_conflict + */ + void minimizeConflictInternal(unsigned low, unsigned high, + std::vector<TNode>& conflict, + std::vector<TNode>& new_conflict); + + bool useHeuristic(); +public: + QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budged = 10000); + ~QuickXPlain(); + Node minimizeConflict(TNode conflict); +}; + +} /* bv namespace */ +} /* theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__BV_QUICK_CHECK_H */ |