dimitri/Civilisation-hs
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Removed unnecessary call in solveDPLL

Browse source
This commit is contained in:
Dimitri Lozeve 2016-08-04 20:11:47 +01:00
parent 9e0c91d0e3
commit 77874cd68a
No known key found for this signature in database
GPG key ID: 12B390E6BD7CF219
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
Sat.hs
View file

@ -219,8 +219,7 @@ solveDPLL (f, asst)
let (f', asst') = (pureLitRule . unitPropagate) (f, asst) in let (f', asst') = (pureLitRule . unitPropagate) (f, asst) in
case solveDPLL (evalLit lit f', lit:asst') of case solveDPLL (evalLit lit f', lit:asst') of
SAT a -> SAT a SAT a -> SAT a
UNSAT -> let (f'', asst'') = (pureLitRule . unitPropagate) (f, asst) in UNSAT -> solveDPLL (evalLit (notLit lit) f', notLit lit : asst')
solveDPLL (evalLit (notLit lit) f'', notLit lit : asst'')
-- Select a literal from a given formula. This function just takes the -- Select a literal from a given formula. This function just takes the
-- first available literal. The function head makes it unsafe, as it -- first available literal. The function head makes it unsafe, as it