-
Notifications
You must be signed in to change notification settings - Fork 4
/
BooleanFormulaWithCosts.html
69 lines (59 loc) · 40.6 KB
/
BooleanFormulaWithCosts.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
<!DOCTYPE html ><html><head><meta http-equiv="X-UA-Compatible" content="IE=edge"/><meta content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no" name="viewport"/><title>delSAT 0.5.2 API - input.BooleanFormulaWithCosts</title><meta content="delSAT 0.5.2 API - input.BooleanFormulaWithCosts" name="description"/><meta content="delSAT 0.5.2 API input.BooleanFormulaWithCosts" name="keywords"/><meta http-equiv="content-type" content="text/html; charset=UTF-8"/><link href="../lib/index.css" media="screen" type="text/css" rel="stylesheet"/><link href="../lib/template.css" media="screen" type="text/css" rel="stylesheet"/><link href="../lib/print.css" media="print" type="text/css" rel="stylesheet"/><link href="../lib/diagrams.css" media="screen" type="text/css" rel="stylesheet" id="diagrams-css"/><script type="text/javascript" src="../lib/jquery.min.js"></script><script type="text/javascript" src="../lib/index.js"></script><script type="text/javascript" src="../index.js"></script><script type="text/javascript" src="../lib/scheduler.js"></script><script type="text/javascript" src="../lib/template.js"></script><script type="text/javascript">/* this variable can be used by the JS to determine the path to the root document */
var toRoot = '../';</script></head><body><div id="search"><span id="doc-title">delSAT 0.5.2 API<span id="doc-version"></span></span> <span class="close-results"><span class="left"><</span> Back</span><div id="textfilter"><span class="input"><input autocapitalize="none" placeholder="Search" id="index-input" type="text" accesskey="/"/><i class="clear material-icons"></i><i id="search-icon" class="material-icons"></i></span></div></div><div id="search-results"><div id="search-progress"><div id="progress-fill"></div></div><div id="results-content"><div id="entity-results"></div><div id="member-results"></div></div></div><div id="content-scroll-container" style="-webkit-overflow-scrolling: touch;"><div id="content-container" style="-webkit-overflow-scrolling: touch;"><div id="subpackage-spacer"><div id="packages"><h1>Packages</h1><ul><li class="indented0 " name="_root_.root" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="_root_"></a><a id="root:_root_"></a> <span class="permalink"><a href="../index.html" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">package</span></span> <span class="symbol"><a href="../index.html" title=""><span class="name">root</span></a></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd><a href="../index.html" name="_root_" id="_root_" class="extype">root</a></dd></dl></div></li><li class="indented1 " name="_root_.input" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="input"></a><a id="input:input"></a> <span class="permalink"><a href="../input/index.html" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">package</span></span> <span class="symbol"><a href="index.html" title="Find User API entry point classes input.ProbabilisticAnswerSetProgram (API for plain or probabilistic Answer Set Programming) and input.BooleanFormulaWithCosts (API for plain or probabilistic SAT solving) here"><span class="name">input</span></a></span><p class="shortcomment cmt">Find User API entry point classes <a href="ProbabilisticAnswerSetProgram.html" name="input.ProbabilisticAnswerSetProgram" id="input.ProbabilisticAnswerSetProgram" class="extype">input.ProbabilisticAnswerSetProgram</a> (API for plain or probabilistic Answer Set Programming) and <a href="" name="input.BooleanFormulaWithCosts" id="input.BooleanFormulaWithCosts" class="extype">input.BooleanFormulaWithCosts</a> (API for plain or probabilistic SAT solving) here
</p><div class="fullcomment"><div class="comment cmt"><p>Find User API entry point classes <a href="ProbabilisticAnswerSetProgram.html" name="input.ProbabilisticAnswerSetProgram" id="input.ProbabilisticAnswerSetProgram" class="extype">input.ProbabilisticAnswerSetProgram</a> (API for plain or probabilistic Answer Set Programming) and <a href="" name="input.BooleanFormulaWithCosts" id="input.BooleanFormulaWithCosts" class="extype">input.BooleanFormulaWithCosts</a> (API for plain or probabilistic SAT solving) here
</p></div><dl class="attributes block"><dt>Definition Classes</dt><dd><a href="../index.html" name="_root_" id="_root_" class="extype">root</a></dd></dl></div></li><li class="current-entities indented1"><span class="separator"></span> <a href="AspifOrDIMACSPlainParserResult.html" title="Result of the aspif or dimacs parser." class="class"></a><a href="AspifOrDIMACSPlainParserResult.html" title="Result of the aspif or dimacs parser.">AspifOrDIMACSPlainParserResult</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="AspifPlainParser$.html" title="Parser for a subset of the ASP Intermediate Format (aspif), enhanced with support for probabilistic rules." class="object"></a><a href="AspifPlainParser$.html" title="Parser for a subset of the ASP Intermediate Format (aspif), enhanced with support for probabilistic rules.">AspifPlainParser</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="BooleanClause.html" title="A disjunctive set of literals (hard clause)" class="class"></a><a href="BooleanClause.html" title="A disjunctive set of literals (hard clause)">BooleanClause</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="" title="A collection of probabilistic and/or non-probabilistic Boolean clauses (disjunctions of literals)" class="class"></a><a href="" title="A collection of probabilistic and/or non-probabilistic Boolean clauses (disjunctions of literals)">BooleanFormulaWithCosts</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="BooleanLiteral.html" title="A literal, represented as a positive or negative integer value." class="class"></a><a href="BooleanLiteral.html" title="A literal, represented as a positive or negative integer value.">BooleanLiteral</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="Clause.html" title="" class="class"></a><a href="Clause.html" title="">Clause</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="DIMACPlainSparser$.html" title="Parser for DIMACS-CNF and PCNF (probabilistic CNF)." class="object"></a><a href="DIMACPlainSparser$.html" title="Parser for DIMACS-CNF and PCNF (probabilistic CNF).">DIMACPlainSparser</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="GroundSymbolicASPRule.html" title="As input.SymbolicASPRule, but without variables." class="class"></a><a href="GroundSymbolicASPRule.html" title="As input.SymbolicASPRule, but without variables.">GroundSymbolicASPRule</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="InputData.html" title="Input data for the sampler/solver" class="class"></a><a href="InputData.html" title="Input data for the sampler/solver">InputData</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="ParseOptimizationTerms$.html" title="" class="object"></a><a href="ParseOptimizationTerms$.html" title="">ParseOptimizationTerms</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="ProbabilisticAnswerSetProgram.html" title="User API representation of a probabilistic or non-probabilistic ASP ground program, consisting of a set of input.GroundSymbolicASPRule rules (for the User API for probabilistic Boolean clauses, see input.BooleanFormulaWithCosts)." class="class"></a><a href="ProbabilisticAnswerSetProgram.html" title="User API representation of a probabilistic or non-probabilistic ASP ground program, consisting of a set of input.GroundSymbolicASPRule rules (for the User API for probabilistic Boolean clauses, see input.BooleanFormulaWithCosts).">ProbabilisticAnswerSetProgram</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="ProbabilisticBooleanClause.html" title="A disjunctive set of literals, annotated with a probability (soft clause)." class="class"></a><a href="ProbabilisticBooleanClause.html" title="A disjunctive set of literals, annotated with a probability (soft clause).">ProbabilisticBooleanClause</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="SolverParametersOverlay.html" title="Solver and sampling settings." class="class"></a><a href="SolverParametersOverlay.html" title="Solver and sampling settings.">SolverParametersOverlay</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="SymbolicASPRule.html" title="Allows to represent all fundamental rule types in Answer Set Programming except weak rules :~." class="class"></a><a href="SymbolicASPRule.html" title="Allows to represent all fundamental rule types in Answer Set Programming except weak rules :~.">SymbolicASPRule</a></li><li class="current-entities indented1"><span class="separator"></span> <a href="diffSAT$.html" title="" class="object"></a><a href="diffSAT$.html" title="">diffSAT</a></li></ul></div></div><div id="content"><body class="class type"><div id="definition"><div class="big-circle class">c</div><p id="owner"><a href="index.html" name="input" id="input" class="extype">input</a></p><h1>BooleanFormulaWithCosts<span class="permalink"><a href="../input/BooleanFormulaWithCosts.html" title="Permalink"><i class="material-icons"></i></a></span></h1><h3><span class="morelinks"></span></h3></div><h4 id="signature" class="signature"><span class="modifier_kind"><span class="modifier"></span> <span class="kind">case class</span></span> <span class="symbol"><span class="name">BooleanFormulaWithCosts</span><span class="params">(<span name="clauses">clauses: <span name="scala.Predef.Set" class="extype">Set</span>[<a href="Clause.html" name="input.Clause" id="input.Clause" class="extype">Clause</a>]</span>, <span name="maxVar">maxVar: <span name="scala.Int" class="extype">Int</span> = <span class="symbol">-1</span></span>)</span><span class="result"> extends <span name="scala.Product" class="extype">Product</span> with <span name="scala.Serializable" class="extype">Serializable</span></span></span></h4><div id="comment" class="fullcommenttop"><div class="comment cmt"><p>A collection of probabilistic and/or non-probabilistic Boolean clauses (disjunctions of literals)</p><p>User API part for probabilistic SAT solving and multimodel optimization (for the User API part for probabilistic Answer Set
Programming see <a href="ProbabilisticAnswerSetProgram.html" name="input.ProbabilisticAnswerSetProgram" id="input.ProbabilisticAnswerSetProgram" class="extype">input.ProbabilisticAnswerSetProgram</a>)</p><p>Example:
Construct CNF and specify multimodel optimization goal:</p><pre><span class="cmt">// The following API calls corresponds to solving the following Enhanced DIMACS CNF file:</span>
<span class="cmt">//</span>
<span class="cmt">// 1 -1 0</span>
<span class="cmt">// 2 -2 0</span>
<span class="cmt">// -1 -2 0</span>
<span class="cmt">//</span>
<span class="cmt">// pats 1 2</span>
<span class="cmt">//</span>
<span class="cmt">// cost (0.2-f(v1))^2</span>
<span class="cmt">// cost (0.5-f(v2))^2</span>
<span class="cmt">//</span>
<span class="kw">val</span> clause1 = BooleanClause(literals = <span class="std">Set</span>(BooleanLiteral(<span class="num">1</span>), BooleanLiteral(-<span class="num">1</span>)))
<span class="kw">val</span> clause2 = BooleanClause(literals = <span class="std">Set</span>(BooleanLiteral(<span class="num">2</span>), BooleanLiteral(-<span class="num">2</span>)))
<span class="kw">val</span> clause3 = BooleanClause(literals = <span class="std">Set</span>(BooleanLiteral(-<span class="num">1</span>), BooleanLiteral(-<span class="num">2</span>)))
<span class="kw">val</span> booleanFormula: BooleanFormulaWithCosts = BooleanFormulaWithCosts(<span class="std">Set</span>(clause1, clause2, clause3))
<span class="kw">val</span> probabilisticObjectives = <span class="cmt">// Parameter atoms are "1" and "2". Atom "1" has probability 0.2, "2" has probability 0.5</span>
<span class="lit">"""pats 1 2
cost (0.2-f(v1))^2
cost (0.5-f(v2))^2
"""
// (Alternatively, cost (loss) terms can be constructed programmatically (see ParseOptimizationTerms to get an idea how to do
// this. Also consider using the ASP User API ([[input.ProbabilisticAnswerSetProgram]]) which allows to work
// with symbolic atoms and rules.)</span></pre><p> Invoke sampler and examine the resulting sample (a set of models):</p><pre><span class="kw">val</span> solverParams = input.SolverParametersOverlay(
noOfModels = -<span class="num">1</span>, <span class="cmt">// -1 means sample until desired accuracy (thresholdOpt) has been reached. A positive</span>
<span class="cmt">// number would specify a minimum sample size (number of answer sets).</span>
noOfSecondaryModels = <span class="num">0</span>,
offHeapGarbageCollectionModeR = <span class="num">0</span>,
thresholdOpt = <span class="std">Some</span>(<span class="num">0.001</span>d), <span class="cmt">// the desired accuracy (lower = more accurate but sampling requires more time)</span>
assureMSE = <span class="kw">true</span>, <span class="cmt">// true = the loss function is assured to be of type MSE (false works too but true is more efficient)</span>
showauxInSATmode = <span class="kw">false</span>,
advancedSolverArgs = mutable.HashMap[(<span class="std">String</span>, <span class="std">Int</span>), <span class="std">String</span>]( <span class="cmt">// advanced solver parameters (corresponding to --solverarg commandline parameters)</span>
(<span class="lit">"seedRngGlobalR"</span>, <span class="num">0</span>) -> <span class="lit">"-1"</span> <span class="cmt">// uses a random PRNG seed seed for each run. Otherwise, we would get the same set of models at each call.</span>
, (<span class="lit">"diversify"</span>, <span class="num">0</span>) -> <span class="lit">"false"</span> <span class="cmt">// "true" increases the entropy - with false, we might get a highly non-uniform distribution if there are no probabilities specified</span>
)
)
<span class="kw">val</span> sampled: SamplingResult = booleanFormula.solve(solverParams,
paramAtomsAndInnerCostsStrOpt = <span class="std">Some</span>(probabilisticObjectives))
<span class="cmt">// Print sample and the result of ad hoc query Pr[p(a):-not q AND p(b):-not q]:</span>
<span class="kw">val</span> (_, adHocConjunctiveQueriesResults, adHocDisjunctiveQueriesResults, adHocRuleQueriesResults,
adHocConjunctionOfSimpleGroundRulesQuery) = delSAT.queryAndPrintSolverResult(showauxInASPmode = <span class="kw">false</span>,
satMode = <span class="kw">true</span>,
samplingResult = sampled,
adHocConjunctiveQueries = <span class="std">Seq</span>(<span class="std">Seq</span>(<span class="lit">"1"</span>), <span class="std">Seq</span>(<span class="lit">"2"</span>)),
adHocDisjunctiveQueries = <span class="std">Seq</span>(),
adHocConjunctionOfSimpleGroundRulesQuery = <span class="std">Seq</span>(),
printAdHocQueryResults = <span class="kw">true</span>,
printAnswers = <span class="kw">true</span>)
println(adHocConjunctiveQueriesResults)</pre><p>Further examples can be found in the source code of <a href="../userAPItests/APITests.html" name="userAPItests.APITests" id="userAPItests.APITests" class="extype">userAPItests.APITests</a>
</p></div><dl class="paramcmts block"><dt class="param">maxVar</dt><dd class="cmt"><p>: largest (by name) propositional variable. If -1 it will be automatically determined.</p></dd></dl><div class="toggleContainer"><div class="toggle block"><span>Linear Supertypes</span><div class="superTypes hiddenContent"><a href="https://docs.oracle.com/javase/8/docs/api/java/io/Serializable.html#java.io.Serializable" name="java.io.Serializable" id="java.io.Serializable" class="extype">Serializable</a>, <span name="scala.Product" class="extype">Product</span>, <span name="scala.Equals" class="extype">Equals</span>, <span name="scala.AnyRef" class="extype">AnyRef</span>, <span name="scala.Any" class="extype">Any</span></div></div></div></div><div id="mbrsel"><div class="toggle"></div><div id="memberfilter"><i class="material-icons arrow"></i><span class="input"><input placeholder="Filter all members" id="mbrsel-input" type="text" accesskey="/"/></span><i class="clear material-icons"></i></div><div id="filterby"><div id="order"><span class="filtertype">Ordering</span><ol><li class="alpha in"><span>Alphabetic</span></li><li class="inherit out"><span>By Inheritance</span></li></ol></div><div class="ancestors"><span class="filtertype">Inherited<br/></span><ol id="linearization"><li class="in" name="input.BooleanFormulaWithCosts"><span>BooleanFormulaWithCosts</span></li><li class="in" name="java.io.Serializable"><span>Serializable</span></li><li class="in" name="scala.Product"><span>Product</span></li><li class="in" name="scala.Equals"><span>Equals</span></li><li class="in" name="scala.AnyRef"><span>AnyRef</span></li><li class="in" name="scala.Any"><span>Any</span></li></ol></div><div class="ancestors"><span class="filtertype"></span><ol><li class="hideall out"><span>Hide All</span></li><li class="showall in"><span>Show All</span></li></ol></div><div id="visbl"><span class="filtertype">Visibility</span><ol><li class="public in"><span>Public</span></li><li class="protected out"><span>Protected</span></li></ol></div></div></div><div id="template"><div id="allMembers"><div id="constructors" class="members"><h3>Instance Constructors</h3><ol><li class="indented0 " name="input.BooleanFormulaWithCosts#<init>" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="<init>(clauses:Set[input.Clause],maxVar:Int):input.BooleanFormulaWithCosts"></a><a id="<init>:BooleanFormulaWithCosts"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#<init>(clauses:Set[input.Clause],maxVar:Int):input.BooleanFormulaWithCosts" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">new</span></span> <span class="symbol"><span class="name">BooleanFormulaWithCosts</span><span class="params">(<span name="clauses">clauses: <span name="scala.Predef.Set" class="extype">Set</span>[<a href="Clause.html" name="input.Clause" id="input.Clause" class="extype">Clause</a>]</span>, <span name="maxVar">maxVar: <span name="scala.Int" class="extype">Int</span> = <span class="symbol">-1</span></span>)</span></span><p class="shortcomment cmt"></p><div class="fullcomment"><div class="comment cmt"></div><dl class="paramcmts block"><dt class="param">maxVar</dt><dd class="cmt"><p>: largest (by name) propositional variable. If -1 it will be automatically determined.</p></dd></dl></div></li></ol></div><div class="values members"><h3>Value Members</h3><ol><li class="indented0 " name="scala.AnyRef#!=" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="!=(x$1:Any):Boolean"></a><a id="!=(Any):Boolean"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#!=(x$1:Any):Boolean" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name" title="gt4s: $bang$eq">!=</span><span class="params">(<span name="arg0">arg0: <span name="scala.Any" class="extype">Any</span></span>)</span><span class="result">: <span name="scala.Boolean" class="extype">Boolean</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef → Any</dd></dl></div></li><li class="indented0 " name="scala.AnyRef###" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="##:Int"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html###:Int" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name" title="gt4s: $hash$hash">##</span><span class="result">: <span name="scala.Int" class="extype">Int</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef → Any</dd></dl></div></li><li class="indented0 " name="scala.AnyRef#==" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="==(x$1:Any):Boolean"></a><a id="==(Any):Boolean"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#==(x$1:Any):Boolean" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name" title="gt4s: $eq$eq">==</span><span class="params">(<span name="arg0">arg0: <span name="scala.Any" class="extype">Any</span></span>)</span><span class="result">: <span name="scala.Boolean" class="extype">Boolean</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef → Any</dd></dl></div></li><li class="indented0 " name="scala.Any#asInstanceOf" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="asInstanceOf[T0]:T0"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#asInstanceOf[T0]:T0" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">asInstanceOf</span><span class="tparams">[<span name="T0">T0</span>]</span><span class="result">: <span name="scala.Any.asInstanceOf.T0" class="extype">T0</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>Any</dd></dl></div></li><li class="indented0 " name="input.BooleanFormulaWithCosts#clauses" group="Ungrouped" fullComment="no" data-isabs="false" visbl="pub"><a id="clauses:Set[input.Clause]"></a><a id="clauses:Set[Clause]"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#clauses:Set[input.Clause]" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">val</span></span> <span class="symbol"><span class="name">clauses</span><span class="result">: <span name="scala.Predef.Set" class="extype">Set</span>[<a href="Clause.html" name="input.Clause" id="input.Clause" class="extype">Clause</a>]</span></span></li><li class="indented0 " name="scala.AnyRef#clone" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="prt"><a id="clone():Object"></a><a id="clone():AnyRef"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#clone():Object" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">def</span></span> <span class="symbol"><span class="name">clone</span><span class="params">()</span><span class="result">: <span name="scala.AnyRef" class="extype">AnyRef</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Attributes</dt><dd>protected[<span name="java.lang" class="extype">lang</span>] </dd><dt>Definition Classes</dt><dd>AnyRef</dd><dt>Annotations</dt><dd><span class="name">@throws</span><span class="args">(<span><span class="defval">classOf[java.lang.CloneNotSupportedException]</span></span>)</span> <span class="name">@native</span><span class="args">()</span> </dd></dl></div></li><li class="indented0 " name="input.BooleanFormulaWithCosts#costsFromProbabilisticClauses" group="Ungrouped" fullComment="no" data-isabs="false" visbl="pub"><a id="costsFromProbabilisticClauses:scala.collection.mutable.ArrayBuffer[String]"></a><a id="costsFromProbabilisticClauses:ArrayBuffer[String]"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#costsFromProbabilisticClauses:scala.collection.mutable.ArrayBuffer[String]" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">val</span></span> <span class="symbol"><span class="name">costsFromProbabilisticClauses</span><span class="result">: <span name="scala.collection.mutable.ArrayBuffer" class="extype">ArrayBuffer</span>[<span name="scala.Predef.String" class="extype">String</span>]</span></span></li><li class="indented0 " name="input.BooleanFormulaWithCosts#directClauseNogoods" group="Ungrouped" fullComment="no" data-isabs="false" visbl="pub"><a id="directClauseNogoods:Array[utils.IntArrayUnsafeS]"></a><a id="directClauseNogoods:Array[IntArrayUnsafeS]"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#directClauseNogoods:Array[utils.IntArrayUnsafeS]" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">val</span></span> <span class="symbol"><span class="name">directClauseNogoods</span><span class="result">: <span name="scala.Array" class="extype">Array</span>[<a href="../utils/IntArrayUnsafeS.html" name="utils.IntArrayUnsafeS" id="utils.IntArrayUnsafeS" class="extype">IntArrayUnsafeS</a>]</span></span></li><li class="indented0 " name="scala.AnyRef#eq" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="eq(x$1:AnyRef):Boolean"></a><a id="eq(AnyRef):Boolean"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#eq(x$1:AnyRef):Boolean" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">eq</span><span class="params">(<span name="arg0">arg0: <span name="scala.AnyRef" class="extype">AnyRef</span></span>)</span><span class="result">: <span name="scala.Boolean" class="extype">Boolean</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef</dd></dl></div></li><li class="indented0 " name="scala.AnyRef#finalize" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="prt"><a id="finalize():Unit"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#finalize():Unit" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">def</span></span> <span class="symbol"><span class="name">finalize</span><span class="params">()</span><span class="result">: <span name="scala.Unit" class="extype">Unit</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Attributes</dt><dd>protected[<span name="java.lang" class="extype">lang</span>] </dd><dt>Definition Classes</dt><dd>AnyRef</dd><dt>Annotations</dt><dd><span class="name">@throws</span><span class="args">(<span><span class="symbol">classOf[java.lang.Throwable]</span></span>)</span> </dd></dl></div></li><li class="indented0 " name="scala.AnyRef#getClass" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="getClass():Class[_]"></a><a id="getClass():Class[_<:AnyRef]"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#getClass():Class[_]" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">getClass</span><span class="params">()</span><span class="result">: <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Class.html#java.lang.Class" name="java.lang.Class" id="java.lang.Class" class="extype">Class</a>[_ <: <span name="scala.AnyRef" class="extype">AnyRef</span>]</span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef → Any</dd><dt>Annotations</dt><dd><span class="name">@native</span><span class="args">()</span> </dd></dl></div></li><li class="indented0 " name="scala.Any#isInstanceOf" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="isInstanceOf[T0]:Boolean"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#isInstanceOf[T0]:Boolean" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">isInstanceOf</span><span class="tparams">[<span name="T0">T0</span>]</span><span class="result">: <span name="scala.Boolean" class="extype">Boolean</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>Any</dd></dl></div></li><li class="indented0 " name="input.BooleanFormulaWithCosts#maxVar" group="Ungrouped" fullComment="no" data-isabs="false" visbl="pub"><a id="maxVar:Int"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#maxVar:Int" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">var</span></span> <span class="symbol"><span class="name">maxVar</span><span class="result">: <span name="scala.Int" class="extype">Int</span></span></span></li><li class="indented0 " name="scala.AnyRef#ne" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="ne(x$1:AnyRef):Boolean"></a><a id="ne(AnyRef):Boolean"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#ne(x$1:AnyRef):Boolean" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">ne</span><span class="params">(<span name="arg0">arg0: <span name="scala.AnyRef" class="extype">AnyRef</span></span>)</span><span class="result">: <span name="scala.Boolean" class="extype">Boolean</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef</dd></dl></div></li><li class="indented0 " name="scala.AnyRef#notify" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="notify():Unit"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#notify():Unit" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">notify</span><span class="params">()</span><span class="result">: <span name="scala.Unit" class="extype">Unit</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef</dd><dt>Annotations</dt><dd><span class="name">@native</span><span class="args">()</span> </dd></dl></div></li><li class="indented0 " name="scala.AnyRef#notifyAll" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="notifyAll():Unit"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#notifyAll():Unit" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">notifyAll</span><span class="params">()</span><span class="result">: <span name="scala.Unit" class="extype">Unit</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef</dd><dt>Annotations</dt><dd><span class="name">@native</span><span class="args">()</span> </dd></dl></div></li><li class="indented0 " name="input.BooleanFormulaWithCosts#originalMaxVar" group="Ungrouped" fullComment="no" data-isabs="false" visbl="pub"><a id="originalMaxVar:Int"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#originalMaxVar:Int" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">val</span></span> <span class="symbol"><span class="name">originalMaxVar</span><span class="result">: <span name="scala.Int" class="extype">Int</span></span></span></li><li class="indented0 " name="input.BooleanFormulaWithCosts#patsFromProbabilisticClauses" group="Ungrouped" fullComment="no" data-isabs="false" visbl="pub"><a id="patsFromProbabilisticClauses:scala.collection.mutable.ArrayBuffer[aspIOutils.Pred]"></a><a id="patsFromProbabilisticClauses:ArrayBuffer[Pred]"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#patsFromProbabilisticClauses:scala.collection.mutable.ArrayBuffer[aspIOutils.Pred]" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">val</span></span> <span class="symbol"><span class="name">patsFromProbabilisticClauses</span><span class="result">: <span name="scala.collection.mutable.ArrayBuffer" class="extype">ArrayBuffer</span>[<a href="../aspIOutils/index.html#Pred=String" name="aspIOutils.Pred" id="aspIOutils.Pred" class="extmbr">Pred</a>]</span></span></li><li class="indented0 " name="scala.Product#productElementNames" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="productElementNames:Iterator[String]"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#productElementNames:Iterator[String]" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">def</span></span> <span class="symbol"><span class="name">productElementNames</span><span class="result">: <span name="scala.Iterator" class="extype">Iterator</span>[<span name="scala.Predef.String" class="extype">String</span>]</span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>Product</dd></dl></div></li><li class="indented0 " name="input.BooleanFormulaWithCosts#solve" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="solve(solverParametersOverlay:input.SolverParametersOverlay,paramAtomsAndInnerCostsStrOpt:Option[String]):solving.SamplingResult"></a><a id="solve(SolverParametersOverlay,Option[String]):SamplingResult"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#solve(solverParametersOverlay:input.SolverParametersOverlay,paramAtomsAndInnerCostsStrOpt:Option[String]):solving.SamplingResult" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier"></span> <span class="kind">def</span></span> <span class="symbol"><span class="name">solve</span><span class="params">(<span name="solverParametersOverlay">solverParametersOverlay: <a href="SolverParametersOverlay.html" name="input.SolverParametersOverlay" id="input.SolverParametersOverlay" class="extype">SolverParametersOverlay</a></span>, <span name="paramAtomsAndInnerCostsStrOpt">paramAtomsAndInnerCostsStrOpt: <span name="scala.Option" class="extype">Option</span>[<span name="scala.Predef.String" class="extype">String</span>] = <span class="symbol">None</span></span>)</span><span class="result">: <a href="../solving/SamplingResult.html" name="solving.SamplingResult" id="solving.SamplingResult" class="extype">SamplingResult</a></span></span><p class="shortcomment cmt">Calls the sampler for this propositional formula.</p><div class="fullcomment"><div class="comment cmt"><p>Calls the sampler for this propositional formula. Optionally with additional multimodel cost terms (in addition
to those generated from any probabilistic clauses)
</p></div><dl class="paramcmts block"><dt class="param">paramAtomsAndInnerCostsStrOpt</dt><dd class="cmt"><p>An optional string with a specification of parameter atoms and cost terms
(see README.md). These costs are in addition to those specified indirectly using
probabilistic clauses.</p></dd><dt>returns</dt><dd class="cmt"><p>SamplingResult The list of models is in SamplingResult.modelsSymbolic. Since sampling
is with replacement, the list represents a multiset of models.</p></dd></dl></div></li><li class="indented0 " name="scala.AnyRef#synchronized" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="synchronized[T0](x$1:=>T0):T0"></a><a id="synchronized[T0](=>T0):T0"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#synchronized[T0](x$1:=>T0):T0" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">synchronized</span><span class="tparams">[<span name="T0">T0</span>]</span><span class="params">(<span name="arg0">arg0: => <span name="java.lang.AnyRef.synchronized.T0" class="extype">T0</span></span>)</span><span class="result">: <span name="java.lang.AnyRef.synchronized.T0" class="extype">T0</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef</dd></dl></div></li><li class="indented0 " name="scala.AnyRef#wait" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="wait():Unit"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#wait():Unit" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">wait</span><span class="params">()</span><span class="result">: <span name="scala.Unit" class="extype">Unit</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef</dd><dt>Annotations</dt><dd><span class="name">@throws</span><span class="args">(<span><span class="defval">classOf[java.lang.InterruptedException]</span></span>)</span> </dd></dl></div></li><li class="indented0 " name="scala.AnyRef#wait" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="wait(x$1:Long,x$2:Int):Unit"></a><a id="wait(Long,Int):Unit"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#wait(x$1:Long,x$2:Int):Unit" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">wait</span><span class="params">(<span name="arg0">arg0: <span name="scala.Long" class="extype">Long</span></span>, <span name="arg1">arg1: <span name="scala.Int" class="extype">Int</span></span>)</span><span class="result">: <span name="scala.Unit" class="extype">Unit</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef</dd><dt>Annotations</dt><dd><span class="name">@throws</span><span class="args">(<span><span class="defval">classOf[java.lang.InterruptedException]</span></span>)</span> </dd></dl></div></li><li class="indented0 " name="scala.AnyRef#wait" group="Ungrouped" fullComment="yes" data-isabs="false" visbl="pub"><a id="wait(x$1:Long):Unit"></a><a id="wait(Long):Unit"></a> <span class="permalink"><a href="../input/BooleanFormulaWithCosts.html#wait(x$1:Long):Unit" title="Permalink"><i class="material-icons"></i></a></span> <span class="modifier_kind"><span class="modifier">final </span> <span class="kind">def</span></span> <span class="symbol"><span class="name">wait</span><span class="params">(<span name="arg0">arg0: <span name="scala.Long" class="extype">Long</span></span>)</span><span class="result">: <span name="scala.Unit" class="extype">Unit</span></span></span><div class="fullcomment"><dl class="attributes block"><dt>Definition Classes</dt><dd>AnyRef</dd><dt>Annotations</dt><dd><span class="name">@throws</span><span class="args">(<span><span class="defval">classOf[java.lang.InterruptedException]</span></span>)</span> <span class="name">@native</span><span class="args">()</span> </dd></dl></div></li></ol></div></div><div id="inheritedMembers"><div name="java.io.Serializable" class="parent"><h3>Inherited from <a href="https://docs.oracle.com/javase/8/docs/api/java/io/Serializable.html#java.io.Serializable" name="java.io.Serializable" id="java.io.Serializable" class="extype">Serializable</a></h3></div><div name="scala.Product" class="parent"><h3>Inherited from <span name="scala.Product" class="extype">Product</span></h3></div><div name="scala.Equals" class="parent"><h3>Inherited from <span name="scala.Equals" class="extype">Equals</span></h3></div><div name="scala.AnyRef" class="parent"><h3>Inherited from <span name="scala.AnyRef" class="extype">AnyRef</span></h3></div><div name="scala.Any" class="parent"><h3>Inherited from <span name="scala.Any" class="extype">Any</span></h3></div></div><div id="groupedMembers"><div name="Ungrouped" class="group"><h3>Ungrouped</h3></div></div></div><div id="tooltip"></div><div id="footer"></div></body></div></div></div></body></html>