diff options
Diffstat (limited to 'src/omt/omt_optimizer.h')
| -rw-r--r-- | src/omt/omt_optimizer.h | 92 |
1 files changed, 67 insertions, 25 deletions
diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h index 792a60169..1052865b0 100644 --- a/src/omt/omt_optimizer.h +++ b/src/omt/omt_optimizer.h @@ -27,54 +27,96 @@ class OMTOptimizer { public: virtual ~OMTOptimizer() = default; + /** - * Given a target node, retrieve an optimizer specific for the node's type - * the second field isSigned specifies whether we should use signed comparison - * for BitVectors and it's only valid when the type is BitVector - * - * @param targetNode the target node for the expression to be optimized - * @param isSigned speficies whether to use signed comparison for BitVectors - * and it's only valid when the type of targetNode is BitVector + * Returns whether node supports optimization + * Currently supported: BitVectors, Integers (preliminary). + * @param node the target node to check for optimizability + * @return whether node supports optimization + **/ + static bool nodeSupportsOptimization(TNode node); + + /** + * Given an optimization objective, + * retrieve an optimizer specific for the optimization target + * @param objective the an OptimizationObjective object containing + * the optimization target, whether it's maximized or minimized + * and whether it's signed for BV (only applies when the target type is BV) * @return a unique_pointer pointing to a derived class of OMTOptimizer * and this is the optimizer for targetNode **/ - static std::unique_ptr<OMTOptimizer> getOptimizerForNode( - TNode targetNode, bool isSigned = false); + static std::unique_ptr<OMTOptimizer> getOptimizerForObjective( + smt::OptimizationObjective& objective); + + /** + * Given the lhs and rhs expressions, with an optimization objective, + * makes an incremental expression stating that + * lhs `better than` rhs + * under the context specified by objective + * for minimize, it would be lhs < rhs + * for maximize, it would be lhs > rhs + * + * Note: the types of lhs and rhs nodes must match or be convertable + * to the type of the optimization target! + * + * @param nm the NodeManager to manage the made expression + * @param lhs the left hand side of the expression + * @param rhs the right hand side of the expression + * @param objective the optimization objective + * stating whether it's maximize / minimize etc. + * @return an expression stating lhs `better than` rhs, + **/ + static Node mkStrongIncrementalExpression( + NodeManager* nm, + TNode lhs, + TNode rhs, + smt::OptimizationObjective& objective); /** - * Initialize an SMT subsolver for offline optimization purpose - * @param parentSMTSolver the parental solver containing the assertions - * @param needsTimeout specifies whether it needs timeout for each single - * query - * @param timeout the timeout value, given in milliseconds (ms) - * @return a unique_pointer of SMT subsolver + * Given the lhs and rhs expressions, with an optimization objective, + * makes an incremental expression stating that + * lhs `better than or equal to` rhs + * under the context specified by objective + * for minimize, it would be lhs <= rhs + * for maximize, it would be lhs >= rhs + * + * Note: the types of lhs and rhs nodes must match or be convertable + * to the type of the optimization target! + * + * @param nm the NodeManager to manage the made expression + * @param lhs the left hand side of the expression + * @param rhs the right hand side of the expression + * @param objective the optimization objective + * stating whether it's maximize / minimize etc. + * @return an expression stating lhs `better than or equal to` rhs, **/ - static std::unique_ptr<SmtEngine> createOptCheckerWithTimeout( - SmtEngine* parentSMTSolver, - bool needsTimeout = false, - unsigned long timeout = 0); + static Node mkWeakIncrementalExpression( + NodeManager* nm, + TNode lhs, + TNode rhs, + smt::OptimizationObjective& objective); /** - * Minimize the target node with constraints encoded in parentSMTSolver + * Minimize the target node with constraints encoded in optChecker * - * @param parentSMTSolver an SMT solver encoding the assertions as the + * @param optChecker an SMT solver encoding the assertions as the * constraints * @param target the target expression to optimize * @return smt::OptimizationResult the result of optimization, containing * whether it's optimal and the optimized value. **/ - virtual smt::OptimizationResult minimize(SmtEngine* parentSMTSolver, + virtual smt::OptimizationResult minimize(SmtEngine* optChecker, TNode target) = 0; /** - * Maximize the target node with constraints encoded in parentSMTSolver + * Maximize the target node with constraints encoded in optChecker * - * @param parentSMTSolver an SMT solver encoding the assertions as the + * @param optChecker an SMT solver encoding the assertions as the * constraints * @param target the target expression to optimize * @return smt::OptimizationResult the result of optimization, containing * whether it's optimal and the optimized value. **/ - virtual smt::OptimizationResult maximize(SmtEngine* parentSMTSolver, + virtual smt::OptimizationResult maximize(SmtEngine* optChecker, TNode target) = 0; }; |